diff options
| author |  coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-05 13:35:31 +0000 |
|---|---|---|
| committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-05 13:35:31 +0000 |
| commit | bb95ebda330d59474bd0793a8d4e0f51face118f (patch) | |
| tree | 9eeb9de737b6645841edd86d2e8554ac5107d633 | |
| parent | 3ffd87f169443d686c98b76668af3fbcb486e28f (diff) | |
Corrige Bug (PR#290)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3989 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | .depend.newcoq | 1 | ||||
| -rw-r--r-- | library/declaremods.ml | 2 | ||||
| -rw-r--r-- | test-suite/modules/PO.v | 7 |
3 files changed, 5 insertions, 5 deletions
diff --git a/.depend.newcoq b/.depend.newcoq index 564ab665c..ff8fbc5d4 100644 --- a/.depend.newcoq +++ b/.depend.newcoq @@ -74,6 +74,7 @@ newtheories/Logic/Eqdep.vo: newtheories/Logic/Eqdep.v newtheories/Logic/Classical_Pred_Type.vo: newtheories/Logic/Classical_Pred_Type.v newtheories/Logic/Classical_Prop.vo newtheories/Logic/Classical_Prop.vo: newtheories/Logic/Classical_Prop.v newtheories/Logic/ProofIrrelevance.vo newtheories/Logic/ClassicalFacts.vo: newtheories/Logic/ClassicalFacts.v +newtheories/Logic/ChoiceFacts.vo: newtheories/Logic/ChoiceFacts.v newtheories/Logic/Berardi.vo: newtheories/Logic/Berardi.v newtheories/Logic/Eqdep_dec.vo: newtheories/Logic/Eqdep_dec.v newtheories/Logic/Decidable.vo: newtheories/Logic/Decidable.v diff --git a/library/declaremods.ml b/library/declaremods.ml index 814d408bf..8d7a783fc 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -588,8 +588,8 @@ let start_library dir = let export_library dir = - let cenv = Global.export dir in let prefix, lib_stack = Lib.end_compilation dir in + let cenv = Global.export dir in let msid = msid_of_prefix prefix in let substitute, keep, _ = Lib.classify_segment lib_stack in cenv,(msid,substitute,keep) diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v index aafbbf2a1..b16ab2809 100644 --- a/test-suite/modules/PO.v +++ b/test-suite/modules/PO.v @@ -15,7 +15,7 @@ Module Type PO. End PO. -Module Pair[X:PO][Y:PO]. +Module Pair[X:PO][Y:PO]<:PO. Definition T:=X.T*Y.T. Definition le:=[p1,p2] (X.le (fst p1) (fst p2)) /\ (Y.le (snd p1) (snd p2)). @@ -23,12 +23,12 @@ Module Pair[X:PO][Y:PO]. Hints Unfold le. Lemma le_refl : (p:T)(le p p). - Auto. + Info Auto. Save. Lemma le_trans : (p1,p2,p3:T)(le p1 p2) -> (le p2 p3) -> (le p1 p3). Unfold le. - Intuition; EAuto. + Intuition; Info EAuto. Save. Lemma le_antis : (p1,p2:T)(le p1 p2) -> (le p2 p1) -> (p1=p2). @@ -60,7 +60,6 @@ Module Type Fmono. Axiom f_mono : (x1,x2:X.T)(X.le x1 x2) -> (Y.le (f x1) (f x2)). End Fmono. - Read Module Nat. |