coq-community / autosubst Goto Github PK

Instance Subst_vl : Subst vl := vl_subst.
Instance HSubst_tm : HSubst vl tm := tm_hsubst.
Instance HSubst_ty : HSubst vl ty := ty_hsubst.

Goal ∀ s x, x.|[s] = x.
(* x is inferred to have type [ty] because that was the last declared instance — swapping the instances changes the type. *)
Abort.

Hint Mode HSubst - +: typeclass_instances.
(* [Hint Mode HSubst - !: typeclass_instances.] would also work in this test, but I can't think of a case where that's preferable. *)
Fail Goal ∀ s x , x.|[s] = x.
Goal ∀ s (x: ty) , x.|[s] = x. Abort.

COQC Autosubst_MMap.v
File "./Autosubst_MMap.v", line 26, characters 0-37:
Error: Some argument names are duplicated: H

make -C theories
make[1]: Entering directory 'src/autosubst-1.6/theories'
coq_makefile -R . Autosubst Autosubst_Derive.v Autosubst.v Autosubst_MMapInstances.v Autosubst_Classes.v Autosubst_Basics.v Autosubst_Lemmas.v Autosubst_MMap.v Autosubst_Tactics.v -o Makefile.coq
make -f Makefile.coq all
make[2]: Entering directory 'src/autosubst-1.6/theories'
COQDEP Autosubst_Lemmas.v
COQDEP Autosubst_Tactics.v
COQDEP Autosubst_MMap.v
COQDEP Autosubst_Classes.v
COQDEP Autosubst_Basics.v
COQDEP Autosubst_MMapInstances.v
COQDEP Autosubst.v
COQDEP Autosubst_Derive.v
COQC Autosubst_Basics.v
File "./Autosubst_Basics.v", line 76, characters 27-40:
Warning: appcontext is deprecated and will be removed in a future version
[deprecated-appcontext,deprecated]
File "./Autosubst_Basics.v", line 78, characters 29-42:
Warning: appcontext is deprecated and will be removed in a future version
[deprecated-appcontext,deprecated]
File "./Autosubst_Basics.v", line 119, characters 11-27:
Warning: appcontext is deprecated and will be removed in a future version
[deprecated-appcontext,deprecated]
fun (f : var -> var) (sigma : var -> list var) =>
nil .: nil .: f >>> f >>> nil .: nil .: f >>> f >>> nil .: nil .: sigma
     : (var -> var) -> (var -> list var) -> var -> list var
File "./Autosubst_Basics.v", line 272, characters 10-26:
Warning: appcontext is deprecated and will be removed in a future version
[deprecated-appcontext,deprecated]
File "./Autosubst_Basics.v", line 276, characters 10-43:
Warning: appcontext is deprecated and will be removed in a future version
[deprecated-appcontext,deprecated]
File "./Autosubst_Basics.v", line 290, characters 6-22:
Warning: appcontext is deprecated and will be removed in a future version
[deprecated-appcontext,deprecated]
File "./Autosubst_Basics.v", line 294, characters 6-39:
Warning: appcontext is deprecated and will be removed in a future version
[deprecated-appcontext,deprecated]
COQC Autosubst_MMap.v
File "./Autosubst_MMap.v", line 26, characters 0-37:
Error: Some argument names are duplicated: H
make[2]: *** [Makefile.coq:272: Autosubst_MMap.vo] Error 1
make[2]: Leaving directory 'src/autosubst-1.6/theories'
make[1]: *** [Makefile:8: all] Error 2
make[1]: Leaving directory 'src/autosubst-1.6/theories'
make: *** [Makefile:21: lib] Error 2

| Fun (s : {bind term in {bind term}})

  s1, s2, t1, t2, u : term
  A : forall sigma : var -> term, pstep s1.[sigma] s2.[sigma]
  B : forall sigma : var -> term, pstep t1.[sigma] t2.[sigma]
  sigma : var -> term
  ============================
  s2.[Fun s2/].[t2/].[sigma] =
  s2.[up sigma].[Fun s2.[up sigma]/].[t2.[sigma]/]