diff options
Diffstat (limited to 'test-suite/success/Hints.v')
| -rw-r--r-- | test-suite/success/Hints.v | 27 |
1 files changed, 24 insertions, 3 deletions
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index e1c74048..4aa00e68 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -23,11 +23,11 @@ Hint Destruct h8 := 4 Hypothesis (_ <= _) => fun H => apply H. (* Checks that local names are accepted *) Section A. - Remark Refl : forall (A : Set) (x : A), x = x. - Proof refl_equal. + Remark Refl : forall (A : Set) (x : A), x = x. + Proof. exact refl_equal. Defined. Definition Sym := sym_equal. Let Trans := trans_equal. - + Hint Resolve Refl: foo. Hint Resolve Sym: bar. Hint Resolve Trans: foo2. @@ -46,3 +46,24 @@ Section A. End A. +Axiom a : forall n, n=0 <-> n<=0. + +Hint Resolve -> a. +Goal forall n, n=0 -> n<=0. +auto. +Qed. + + +(* This example comes from Chlipala's ltamer *) +(* It used to fail from r12902 to r13112 since type_of started to call *) +(* e_cumul (instead of conv_leq) which was not able to unify "?id" and *) +(* "(fun x => x) ?id" *) + +Notation "e :? pf" := (eq_rect _ (fun X : Set => X) e _ pf) + (no associativity, at level 90). + +Axiom cast_coalesce : + forall (T1 T2 T3 : Set) (e : T1) (pf1 : T1 = T2) (pf2 : T2 = T3), + ((e :? pf1) :? pf2) = (e :? trans_eq pf1 pf2). + +Hint Rewrite cast_coalesce : ltamer. |