diff options
Diffstat (limited to 'test-suite/modules/modul.v')
-rw-r--r-- | test-suite/modules/modul.v | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/test-suite/modules/modul.v b/test-suite/modules/modul.v new file mode 100644 index 00000000..5612ea75 --- /dev/null +++ b/test-suite/modules/modul.v @@ -0,0 +1,39 @@ +Module M. + Parameter rel:nat -> nat -> Prop. + + Axiom w : (n:nat)(rel O (S n)). + + Hints Resolve w. + + Grammar constr constr8 := + not_eq [ constr7($a) "#" constr7($b) ] -> [ (rel $a $b) ]. + + Print Hint *. + + Lemma w1 : (O#(S O)). + Auto. + Save. + +End M. + +(*Lemma w1 : (M.rel O (S O)). +Auto. +*) + +Import M. + +Print Hint *. +Lemma w1 : (O#(S O)). +Print Hint. +Print Hint *. + +Auto. +Save. + +Check (O#O). +Locate rel. + +Locate M. + +Module N:=Top.M. + |