diff options
author | 2006-04-28 14:59:16 +0000 | |
---|---|---|
committer | 2006-04-28 14:59:16 +0000 | |
commit | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch) | |
tree | ad89c6bb57ceee608fcba2bb3435b74e0f57919e /test-suite/modules/modul.v | |
parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) |
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
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. |