From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- test-suite/success/Hints.v | 48 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 48 insertions(+) create mode 100644 test-suite/success/Hints.v (limited to 'test-suite/success/Hints.v') diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v new file mode 100644 index 00000000..f32753e0 --- /dev/null +++ b/test-suite/success/Hints.v @@ -0,0 +1,48 @@ +(* Checks syntax of Hints commands *) +(* 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. + +(* 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. + +(* 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 ]. + +(* Checks that local names are accepted *) +Section A. + Remark Refl : (A:Set)(x:A)x=x. + Proof refl_equal. + Definition Sym := sym_equal. + Local Trans := trans_equal. + + Hint h1 : foo := Resolve Refl. + Hint h2 : bar := Resolve Sym. + Hint h3 : foo2 := Resolve Trans. + + Hint h2 := Immediate Refl. + Hint h2 := Immediate Sym. + Hint h2 := Immediate Trans. + + Hint h3 := Unfold Refl. + Hint h3 := Unfold Sym. + Hint h3 := Unfold Trans. + + Hints Resolve Sym Trans Refl. + Hints Immediate Sym Trans Refl. + Hints Unfold Sym Trans Refl. + +End A. + -- cgit v1.2.3