Merge branch 'v8.5'

2 files changed, 39 insertions, 21 deletions

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index f2e6877989..63c45116a6 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -185,7 +185,7 @@ let look_for_possibly_mutual_statements = function
 
 (* Saving a goal *)
 
-let save id const cstrs do_guard (locality,poly,kind) hook =
+let save ?export_seff id const cstrs do_guard (locality,poly,kind) hook =
   let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
   try
     let const = adjust_guardness_conditions const do_guard in
@@ -200,7 +200,8 @@ let save id const cstrs do_guard (locality,poly,kind) hook =
           | Local | Discharge -> true
           | Global -> false
           in
-          let kn = declare_constant id ~local (DefinitionEntry const, k) in
+          let kn =
+           declare_constant ?export_seff id ~local (DefinitionEntry const, k) in
           (locality, ConstRef kn) in
     definition_message id;
     call_hook (fun exn -> exn) hook l r
@@ -273,25 +274,25 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im
 let save_hook = ref ignore
 let set_save_hook f = save_hook := f
 
-let save_named proof =
+let save_named ?export_seff proof =
   let id,const,cstrs,do_guard,persistence,hook = proof in
-  save id const cstrs do_guard persistence hook
+  save ?export_seff id const cstrs do_guard persistence hook
 
 let check_anonymity id save_ident =
   if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then
     error "This command can only be used for unnamed theorem."
 
 
-let save_anonymous proof save_ident =
+let save_anonymous ?export_seff proof save_ident =
   let id,const,cstrs,do_guard,persistence,hook = proof in
   check_anonymity id save_ident;
-  save save_ident const cstrs do_guard persistence hook
+  save ?export_seff save_ident const cstrs do_guard persistence hook
 
-let save_anonymous_with_strength proof kind save_ident =
+let save_anonymous_with_strength ?export_seff proof kind save_ident =
   let id,const,cstrs,do_guard,_,hook = proof in
   check_anonymity id save_ident;
   (* we consider that non opaque behaves as local for discharge *)
-  save save_ident const cstrs do_guard (Global, const.const_entry_polymorphic, Proof kind) hook
+  save ?export_seff save_ident const cstrs do_guard (Global, const.const_entry_polymorphic, Proof kind) hook
 
 (* Admitted *)
 
@@ -325,34 +326,50 @@ let get_proof proof do_guard hook opacity =
   (** FIXME *)
   id,{const with const_entry_opaque = opacity},cstrs,do_guard,persistence,hook
 
+let check_exist =
+  List.iter (fun (loc,id) ->
+    if not (Nametab.exists_cci (Lib.make_path id)) then
+        user_err_loc (loc,"",pr_id id ++ str " does not exist.")
+  )
+
 let standard_proof_terminator compute_guard hook =
   let open Proof_global in function
   | Admitted ->
       admit hook ();
       Pp.feedback Feedback.AddedAxiom
-  | Proved (is_opaque,idopt,proof) ->
+  | Proved (opaque,idopt,proof) ->
+      let is_opaque, export_seff, exports = match opaque with
+        | Vernacexpr.Transparent -> false, true, []
+        | Vernacexpr.Opaque None -> true, false, []
+        | Vernacexpr.Opaque (Some l) -> true, true, l in
       let proof = get_proof proof compute_guard hook is_opaque in
       begin match idopt with
-      | None -> save_named proof
-      | Some ((_,id),None) -> save_anonymous proof id
+      | None -> save_named ~export_seff proof
+      | Some ((_,id),None) -> save_anonymous ~export_seff proof id
       | Some ((_,id),Some kind) -> 
-          save_anonymous_with_strength proof kind id
-      end
+          save_anonymous_with_strength ~export_seff proof kind id
+      end;
+      check_exist exports
 
 let universe_proof_terminator compute_guard hook =
   let open Proof_global in function
   | Admitted ->
       admit (hook None) ();
       Pp.feedback Feedback.AddedAxiom
-  | Proved (is_opaque,idopt,proof) ->
+  | Proved (opaque,idopt,proof) ->
+      let is_opaque, export_seff, exports = match opaque with
+        | Vernacexpr.Transparent -> false, true, []
+        | Vernacexpr.Opaque None -> true, false, []
+        | Vernacexpr.Opaque (Some l) -> true, true, l in
       let proof = get_proof proof compute_guard 
 	(hook (Some proof.Proof_global.universes)) is_opaque in
       begin match idopt with
-      | None -> save_named proof
-      | Some ((_,id),None) -> save_anonymous proof id
+      | None -> save_named ~export_seff proof
+      | Some ((_,id),None) -> save_anonymous ~export_seff proof id
       | Some ((_,id),Some kind) -> 
-          save_anonymous_with_strength proof kind id
-      end
+          save_anonymous_with_strength ~export_seff proof kind id
+      end;
+      check_exist exports
 
 let start_proof id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
   let terminator = standard_proof_terminator compute_guard hook in
diff --git a/stm/stm.ml b/stm/stm.ml
index 693c673b40..207afd8aee 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1035,7 +1035,7 @@ end = struct (* {{{ *)
         vernac_interp stop
           ~proof:(pobject, terminator)
           { verbose = false; loc;
-            expr = (VernacEndProof (Proved (true,None))) }) in
+            expr = (VernacEndProof (Proved (Opaque None,None))) }) in
       ignore(Future.join checked_proof);
       RespBuiltProof(proof,time)
     with
@@ -1166,7 +1166,7 @@ end = struct (* {{{ *)
       Reach.known_state ~cache:`No start;
       vernac_interp stop ~proof
         { verbose = false; loc;
-          expr = (VernacEndProof (Proved (true,None))) };
+          expr = (VernacEndProof (Proved (Opaque None,None))) };
       Some proof
     with e ->
       let (e, info) = Errors.push e in
@@ -1564,7 +1564,8 @@ let collect_proof keep cur hd brkind id =
    | id :: _ -> Id.to_string id in
  let loc = (snd cur).loc in
  let is_defined = function
-   | _, { expr = VernacEndProof (Proved (false,_)) } -> true
+   | _, { expr = VernacEndProof (Proved ((Transparent|Opaque (Some _)),_)) } ->
+      true
    | _ -> false in
  let proof_using_ast = function
    | Some (_, ({ expr = VernacProof(_,Some _) } as v)) -> Some v