Local universes for opaque polymorphic constants.

2 files changed, 24 insertions, 15 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 9359ab15e2..74e951b3b6 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -20,6 +20,8 @@ let stm_pperr_endline s = if !stm_debug then begin stm_pp_err (s ()) end else ()
 
 let stm_prerr_debug   s = if !Flags.debug then begin stm_pr_err (s ()) end else ()
 
+let is_vtkeep = function Vernacextend.VtKeep _ -> true | _ -> false
+
 open Pp
 open CErrors
 open Names
@@ -1532,12 +1534,13 @@ end = struct (* {{{ *)
       let st = Vernacstate.freeze_interp_state `No in
       if not drop then begin
         let checked_proof = Future.chain future_proof (fun p ->
+          let opaque = Proof_global.Opaque in
 
           (* Unfortunately close_future_proof and friends are not pure so we need
              to set the state manually here *)
           Vernacstate.unfreeze_interp_state st;
           let pobject, _ =
-            Proof_global.close_future_proof ~feedback_id:stop (Future.from_val ~fix_exn p) in
+            Proof_global.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in
           let terminator = (* The one sent by master is an InvalidKey *)
             Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in
 
@@ -1545,7 +1548,7 @@ end = struct (* {{{ *)
           stm_vernac_interp stop
             ~proof:(pobject, terminator) st
             { verbose = false; loc; indentation = 0; strlen = 0;
-              expr = VernacExpr ([], VernacEndProof (Proved (Proof_global.Opaque,None))) }) in
+              expr = VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in
         ignore(Future.join checked_proof);
       end;
       (* STATE: Restore the state XXX: handle exn *)
@@ -1680,9 +1683,10 @@ end = struct (* {{{ *)
       (* The original terminator, a hook, has not been saved in the .vio*)
       Proof_global.set_terminator
         (Lemmas.standard_proof_terminator []
-          (Lemmas.mk_hook (fun _ _ -> ())));
+           (Lemmas.mk_hook (fun _ _ -> ())));
+      let opaque = Proof_global.Opaque in
       let proof =
-        Proof_global.close_proof ~keep_body_ucst_separate:true (fun x -> x) in
+        Proof_global.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in
       (* We jump at the beginning since the kernel handles side effects by also
        * looking at the ones that happen to be present in the current env *)
       Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:`No start;
@@ -1695,7 +1699,7 @@ end = struct (* {{{ *)
       let st = Vernacstate.freeze_interp_state `No in
       ignore(stm_vernac_interp stop ~proof st
         { verbose = false; loc; indentation = 0; strlen = 0;
-          expr = VernacExpr ([], VernacEndProof (Proved (Proof_global.Opaque,None))) });
+          expr = VernacExpr ([], VernacEndProof (Proved (opaque,None))) });
       `OK proof
       end
     with e ->
@@ -2252,7 +2256,7 @@ let collect_proof keep cur hd brkind id =
      else
        let rc = collect (Some cur) [] id in
        if is_empty rc then make_sync `AlreadyEvaluated rc
-       else if (keep == VtKeep || keep == VtKeepAsAxiom) &&
+       else if (is_vtkeep keep || keep == VtKeepAsAxiom) &&
           (not(State.is_cached_and_valid id) || !cur_opt.async_proofs_full)
        then check_policy rc
        else make_sync `AlreadyEvaluated rc
@@ -2441,7 +2445,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
       | `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) ->
           let rec aux = function
           | `ASync (block_start, nodes, name, delegate) -> (fun () ->
-                assert(keep == VtKeep || keep == VtKeepAsAxiom);
+                assert(is_vtkeep keep || keep == VtKeepAsAxiom);
                 let drop_pt = keep == VtKeepAsAxiom in
                 let block_stop, exn_info, loc = eop, (id, eop), x.loc in
                 log_processing_async id name;
@@ -2450,11 +2454,11 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                 | { VCS.kind = `Edit _ }, None -> assert false
                 | { VCS.kind = `Edit (_,_,_, okeep, _) }, Some (ofp, cancel) ->
                     assert(redefine_qed = true);
-                    if okeep != keep then
+                    if okeep <> keep then
                       msg_warning(strbrk("The command closing the proof changed. "
                         ^"The kernel cannot take this into account and will "
-                        ^(if keep == VtKeep then "not check " else "reject ")
-                        ^"the "^(if keep == VtKeep then "new" else "incomplete")
+                        ^(if is_vtkeep keep then "not check " else "reject ")
+                        ^"the "^(if is_vtkeep keep then "new" else "incomplete")
                         ^" proof. Reprocess the command declaring "
                         ^"the proof's statement to avoid that."));
                     let fp, cancel =
@@ -2477,8 +2481,12 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                           ~drop_pt exn_info block_stop, ref false
                     in
                     qed.fproof <- Some (fp, cancel);
+                    let opaque = match keep with
+                      | VtKeep opaque -> opaque
+                      | _ -> Proof_global.Opaque (* this seems strange *)
+                    in
                     let proof =
-                      Proof_global.close_future_proof ~feedback_id:id fp in
+                      Proof_global.close_future_proof ~opaque ~feedback_id:id fp in
                     if not delegate then ignore(Future.compute fp);
                     reach view.next;
                     let st = Vernacstate.freeze_interp_state `No in
@@ -2506,8 +2514,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                       let ctx = UState.empty in
                       let fp = Future.from_val ([],ctx) in
                       qed.fproof <- Some (fp, ref false); None
-                  | VtKeep ->
-                      Some(Proof_global.close_proof
+                  | VtKeep opaque ->
+                      Some(Proof_global.close_proof ~opaque
                                 ~keep_body_ucst_separate:false
                                 (State.exn_on id ~valid:eop)) in
                 if keep != VtKeepAsAxiom then
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 526858bd73..e026539751 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -26,7 +26,7 @@ let string_of_vernac_type = function
   | VtUnknown -> "Unknown"
   | VtStartProof _ -> "StartProof"
   | VtSideff _ -> "Sideff"
-  | VtQed VtKeep -> "Qed(keep)"
+  | VtQed (VtKeep _) -> "Qed(keep)"
   | VtQed VtKeepAsAxiom -> "Qed(admitted)"
   | VtQed VtDrop -> "Qed(drop)"
   | VtProofStep { parallel; proof_block_detection } ->
@@ -66,7 +66,8 @@ let classify_vernac e =
     (* Qed *)
     | VernacAbort _ -> VtQed VtDrop, VtLater
     | VernacEndProof Admitted -> VtQed VtKeepAsAxiom, VtLater
-    | VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater
+    | VernacEndProof (Proved (opaque,_)) -> VtQed (VtKeep opaque), VtLater
+    | VernacExactProof _ -> VtQed (VtKeep Proof_global.Opaque), VtLater
     (* Query *)
     | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _
     | VernacCheckMayEval _ -> VtQuery, VtLater