diff options
Diffstat (limited to 'test-suite/modules/modul.v')
| -rw-r--r-- | test-suite/modules/modul.v | 34 |
1 files changed, 15 insertions, 19 deletions
diff --git a/test-suite/modules/modul.v b/test-suite/modules/modul.v index 84942da1..9d24d6ce 100644 --- a/test-suite/modules/modul.v +++ b/test-suite/modules/modul.v @@ -1,39 +1,35 @@ Module M. - Parameter rel:nat -> nat -> Prop. + Parameter rel : nat -> nat -> Prop. - Axiom w : (n:nat)(rel O (S n)). + Axiom w : forall n : nat, rel 0 (S n). - Hints Resolve w. + Hint Resolve w. - Grammar constr constr8 := - not_eq [ constr7($a) "#" constr7($b) ] -> [ (rel $a $b) ]. + (* <Warning> : Grammar is replaced by Notation *) Print Hint *. - Lemma w1 : (O#(S O)). - Auto. - Save. + Lemma w1 : rel 0 1. + auto. + Qed. End M. +Locate Module M. + (*Lemma w1 : (M.rel O (S O)). Auto. *) Import M. -Print Hint *. -Lemma w1 : (O#(S O)). -Print Hint. -Print Hint *. - -Auto. -Save. +Lemma w1 : rel 0 1. +auto. +Qed. -Check (O#O). +Check (rel 0 0). Locate rel. -Locate Library M. - -Module N:=Top.M. +Locate Module M. +Module N := Top.M. |