Correct rebase on STM code. Thanks to E. Tassi for help on dealing with

latent universes. Now the universes in the type of a definition/lemma
are eagerly added to the environment so that later proofs can be checked
independently of the original (delegated) proof body.

- Fixed firstorder, ring to work correctly with universe polymorphism.
- Changed constr_of_global to raise an anomaly if side effects would be lost by
turning a polymorphic constant into a constr.
- Fix a non-termination issue in solve_evar_evar.
-

1 files changed, 14 insertions, 8 deletions

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 94268e020..76ef10e85 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -46,6 +46,11 @@ let elide_part_of_script_and_now (a, _) =
   | VtStm (x, _) -> VtStm (x, false), VtNow
   | x -> x, VtNow
 
+let make_polymorphic (a, b as x) =
+  match a with
+  | VtStartProof (x, y, ids, _) -> (VtStartProof (x, y, ids, true), b)
+  | _ -> x
+
 let undo_classifier = ref (fun _ -> assert false)
 let set_undo_classifier f = undo_classifier := f
 
@@ -68,7 +73,7 @@ let rec classify_vernac e =
     | VernacLocal (_,e) -> classify_vernac e
     | VernacPolymorphic (b, e) -> 
       if b || Flags.is_universe_polymorphism () (* Ok or not? *) then
-	fst (classify_vernac e), VtNow
+	make_polymorphic (classify_vernac e)
       else classify_vernac e
     | VernacTimeout (_,e) -> classify_vernac e
     | VernacTime e -> classify_vernac e
@@ -88,8 +93,8 @@ let rec classify_vernac e =
     | VernacProof _ 
     | VernacBullet _ 
     | VernacFocus _ | VernacUnfocus
-    | VernacSubproof _ | VernacEndSubproof 
-    | VernacSolve _ | VernacError _
+    | VernacSubproof _ | VernacEndSubproof
+    | VernacSolve _ 
     | VernacCheckGuard
     | VernacUnfocused
     | VernacSolveExistential _ -> VtProofStep, VtLater
@@ -98,23 +103,23 @@ let rec classify_vernac e =
     | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
     (* StartProof *)
     | VernacDefinition (_,(_,i),ProveBody _) ->
-        VtStartProof("Classic",GuaranteesOpacity,[i]), VtLater
+        VtStartProof("Classic",GuaranteesOpacity,[i], false), VtLater
     | VernacStartTheoremProof (_,l,_) ->
         let ids = 
           CList.map_filter (function (Some(_,i), _) -> Some i | _ -> None) l in
-        VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
-    | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater
+        VtStartProof ("Classic",GuaranteesOpacity,ids, false), VtLater
+    | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[],false), VtLater
     | VernacFixpoint (_,l) ->
         let ids, open_proof =
           List.fold_left (fun (l,b) (((_,id),_,_,_,p),_) ->
             id::l, b || p = None) ([],false) l in
-        if open_proof then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
+        if open_proof then VtStartProof ("Classic",GuaranteesOpacity,ids, false), VtLater
         else VtSideff ids, VtLater
     | VernacCoFixpoint (_,l) ->
         let ids, open_proof =
           List.fold_left (fun (l,b) (((_,id),_,_,p),_) ->
             id::l, b || p = None) ([],false) l in
-        if open_proof then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
+        if open_proof then VtStartProof ("Classic",GuaranteesOpacity,ids,false), VtLater
         else VtSideff ids, VtLater
     (* Sideff: apply to all open branches. usually run on master only *)
     | VernacAssumption (_,_,l) ->
@@ -182,6 +187,7 @@ let rec classify_vernac e =
     | VernacToplevelControl _
     | VernacRestoreState _
     | VernacWriteState _ -> VtUnknown, VtNow
+    | VernacError _ -> assert false
     (* Plugins should classify their commands *)
     | VernacExtend (s,l) ->
         try List.assoc s !classifiers l ()