summaryrefslogtreecommitdiff
path: root/test-suite/success/Hints.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
commit3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch)
treead89c6bb57ceee608fcba2bb3435b74e0f57919e /test-suite/success/Hints.v
parent018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff)
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'test-suite/success/Hints.v')
-rw-r--r--test-suite/success/Hints.v56
1 files changed, 28 insertions, 28 deletions
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index f32753e0..e1c74048 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -2,47 +2,47 @@
(* Checks that qualified names are accepted *)
(* New-style syntax *)
-Hint h1 : core arith := Resolve Logic.refl_equal.
-Hint h2 := Immediate Logic.trans_equal.
-Hint h3 : core := Unfold Logic.sym_equal.
-Hint h4 : foo bar := Constructors Logic.eq.
-Hint h5 : foo bar := Extern 3 (eq ? ? ?) Apply Logic.refl_equal.
+Hint Resolve refl_equal: core arith.
+Hint Immediate trans_equal.
+Hint Unfold sym_equal: core.
+Hint Constructors eq: foo bar.
+Hint Extern 3 (_ = _) => apply refl_equal: foo bar.
(* Old-style syntax *)
-Hints Resolve Coq.Init.Logic.refl_equal Coq.Init.Logic.sym_equal.
-Hints Resolve Coq.Init.Logic.refl_equal Coq.Init.Logic.sym_equal : foo.
-Hints Immediate Coq.Init.Logic.refl_equal Coq.Init.Logic.sym_equal.
-Hints Immediate Coq.Init.Logic.refl_equal Coq.Init.Logic.sym_equal : foo.
-Hints Unfold Coq.Init.Datatypes.fst Coq.Init.Logic.sym_equal.
-Hints Unfold Coq.Init.Datatypes.fst Coq.Init.Logic.sym_equal : foo.
+Hint Resolve refl_equal sym_equal.
+Hint Resolve refl_equal sym_equal: foo.
+Hint Immediate refl_equal sym_equal.
+Hint Immediate refl_equal sym_equal: foo.
+Hint Unfold fst sym_equal.
+Hint Unfold fst sym_equal: foo.
(* What's this stranged syntax ? *)
-HintDestruct Conclusion h6 (le ? ?) 4 [ Fun H -> Apply H ].
-HintDestruct Discardable Hypothesis h7 (le ? ?) 4 [ Fun H -> Apply H ].
-HintDestruct Hypothesis h8 (le ? ?) 4 [ Fun H -> Apply H ].
+Hint Destruct h6 := 4 Conclusion (_ <= _) => fun H => apply H.
+Hint Destruct h7 := 4 Discardable Hypothesis (_ <= _) => fun H => apply H.
+Hint Destruct h8 := 4 Hypothesis (_ <= _) => fun H => apply H.
(* Checks that local names are accepted *)
Section A.
- Remark Refl : (A:Set)(x:A)x=x.
+ Remark Refl : forall (A : Set) (x : A), x = x.
Proof refl_equal.
Definition Sym := sym_equal.
- Local Trans := trans_equal.
+ Let Trans := trans_equal.
- Hint h1 : foo := Resolve Refl.
- Hint h2 : bar := Resolve Sym.
- Hint h3 : foo2 := Resolve Trans.
+ Hint Resolve Refl: foo.
+ Hint Resolve Sym: bar.
+ Hint Resolve Trans: foo2.
- Hint h2 := Immediate Refl.
- Hint h2 := Immediate Sym.
- Hint h2 := Immediate Trans.
+ Hint Immediate Refl.
+ Hint Immediate Sym.
+ Hint Immediate Trans.
- Hint h3 := Unfold Refl.
- Hint h3 := Unfold Sym.
- Hint h3 := Unfold Trans.
+ Hint Unfold Refl.
+ Hint Unfold Sym.
+ Hint Unfold Trans.
- Hints Resolve Sym Trans Refl.
- Hints Immediate Sym Trans Refl.
- Hints Unfold Sym Trans Refl.
+ Hint Resolve Sym Trans Refl.
+ Hint Immediate Sym Trans Refl.
+ Hint Unfold Sym Trans Refl.
End A.