Merge branch 'v8.5'

2 files changed, 4 insertions, 21 deletions

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 6c86304041..a7ef96c668 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -326,25 +326,6 @@ let check_exist =
         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 (id,k,pe,_) ->
-      admit (id,k,pe) hook ();
-      Pp.feedback Feedback.AddedAxiom
-  | 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 ~export_seff proof
-      | Some ((_,id),None) -> save_anonymous ~export_seff proof id
-      | Some ((_,id),Some kind) -> 
-          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 (id,k,pe,ctx) ->
@@ -365,6 +346,9 @@ let universe_proof_terminator compute_guard hook =
       end;
       check_exist exports
 
+let standard_proof_terminator compute_guard hook =
+  universe_proof_terminator compute_guard (fun _ -> hook)
+
 let start_proof id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
   let terminator = standard_proof_terminator compute_guard hook in
   let sign = 
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
index a0ddd265cb..6556aa2297 100644
--- a/stm/lemmas.mli
+++ b/stm/lemmas.mli
@@ -32,8 +32,7 @@ val start_proof_univs : Id.t -> goal_kind -> Evd.evar_map -> ?sign:Environ.named
   ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
   (Proof_global.proof_universes option -> unit declaration_hook) -> unit
 
-val start_proof_com : goal_kind ->
-  (lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)) list ->
+val start_proof_com : goal_kind -> Vernacexpr.proof_expr list ->
   unit declaration_hook -> unit
 
 val start_proof_with_initialization :