Imported Upstream version 8.5~beta3+dfsg

1 files changed, 67 insertions, 35 deletions

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 5bff3c81..c303f486 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -67,14 +67,14 @@ type proof_universes = Evd.evar_universe_context
 
 type proof_object = {
   id : Names.Id.t;
-  entries : Entries.definition_entry list;
+  entries : Safe_typing.private_constants Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
   universes: proof_universes;
   (* constraints : Univ.constraints; *)
 }
 
 type proof_ending =
-  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry
+  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes
   | Proved of Vernacexpr.opacity_flag *
              (Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
               proof_object
@@ -250,17 +250,43 @@ let start_dependent_proof id str goals terminator =
 
 let get_used_variables () = (cur_pstate ()).section_vars
 
+let proof_using_auto_clear = ref true
+let _ = Goptions.declare_bool_option
+    { Goptions.optsync  = true;
+      Goptions.optdepr  = false;
+      Goptions.optname  = "Proof using Clear Unused";
+      Goptions.optkey   = ["Proof";"Using";"Clear";"Unused"];
+      Goptions.optread  = (fun () -> !proof_using_auto_clear);
+      Goptions.optwrite = (fun b -> proof_using_auto_clear := b) }
+
 let set_used_variables l =
   let env = Global.env () in
   let ids = List.fold_right Id.Set.add l Id.Set.empty in
   let ctx = Environ.keep_hyps env ids in
+  let ctx_set =
+    List.fold_right Id.Set.add (List.map pi1 ctx) Id.Set.empty in
+  let vars_of = Environ.global_vars_set in
+  let aux env entry (ctx, all_safe, to_clear as orig) =
+    match entry with
+    | (x,None,_) ->
+       if Id.Set.mem x all_safe then orig
+       else (ctx, all_safe, (Loc.ghost,x)::to_clear) 
+    | (x,Some bo, ty) as decl ->
+       if Id.Set.mem x all_safe then orig else
+       let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in
+       if Id.Set.subset vars all_safe
+       then (decl :: ctx, Id.Set.add x all_safe, to_clear)
+       else (ctx, all_safe, (Loc.ghost,x) :: to_clear) in
+  let ctx, _, to_clear =
+    Environ.fold_named_context aux env ~init:(ctx,ctx_set,[]) in
+  let to_clear = if !proof_using_auto_clear then to_clear else [] in
   match !pstates with
   | [] -> raise NoCurrentProof
   | p :: rest ->
       if not (Option.is_empty p.section_vars) then
         Errors.error "Used section variables can be declared only once";
       pstates := { p with section_vars = Some ctx} :: rest;
-      ctx
+      ctx, to_clear
 
 let get_open_goals () =
   let gl, gll, shelf , _ , _ = Proof.proof (cur_pstate ()).proof in
@@ -269,16 +295,14 @@ let get_open_goals () =
     (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) +
     List.length shelf
 
-let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl =
+let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
   let { pid; section_vars; strength; proof; terminator } = cur_pstate () in
   let poly = pi2 strength (* Polymorphic *) in
   let initial_goals = Proof.initial_goals proof in
+  let initial_euctx = Proof.initial_euctx proof in
   let fpl, univs = Future.split2 fpl in
-  let universes = 
-    if poly || now then Future.force univs 
-    else Proof.in_proof proof (fun x -> Evd.evar_universe_context x) 
-  in
-  (* Because of dependent subgoals at the begining of proofs, we could
+  let universes = if poly || now then Future.force univs else initial_euctx in
+  (* Because of dependent subgoals at the beginning of proofs, we could
      have existential variables in the initial types of goals, we need to
      normalise them for the kernel. *)
   let subst_evar k =
@@ -289,19 +313,26 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl =
     if poly || now then
       let make_body t (c, eff) =
         let open Universes in
-	let body = c and typ = nf t in
+        let body = c in
+	let typ =
+	  if not (keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff)) then
+	    nf t
+	  else t
+	in
         let used_univs_body = Universes.universes_of_constr body in
-	let used_univs_typ = Universes.universes_of_constr typ in
-	let ctx = Evd.evar_universe_context_set universes in
-        if keep_body_ucst_sepatate then
+        let used_univs_typ = Universes.universes_of_constr typ in
+        if keep_body_ucst_separate ||
+           not (Safe_typing.empty_private_constants = eff) then
+          let initunivs = Evd.evar_context_universe_context initial_euctx in
+          let ctx = Evd.evar_universe_context_set initunivs universes in
           (* For vi2vo compilation proofs are computed now but we need to
            * complement the univ constraints of the typ with the ones of
            * the body.  So we keep the two sets distinct. *)
           let ctx_body = restrict_universe_context ctx used_univs_body in
-          let ctx_typ = restrict_universe_context ctx used_univs_typ in
-          let univs_typ = Univ.ContextSet.to_context ctx_typ in
-          (univs_typ, typ), ((body, ctx_body), eff)
+          (initunivs, typ), ((body, ctx_body), eff)
         else
+          let initunivs = Univ.UContext.empty in
+          let ctx = Evd.evar_universe_context_set initunivs universes in
           (* Since the proof is computed now, we can simply have 1 set of
            * constraints in which we merge the ones for the body and the ones
            * for the typ *)
@@ -310,14 +341,13 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl =
           let univs = Univ.ContextSet.to_context ctx in
           (univs, typ), ((body, Univ.ContextSet.empty), eff)
       in 
-	fun t p ->
-	  Future.split2 (Future.chain ~pure:true p (make_body t))
+       fun t p -> Future.split2 (Future.chain ~pure:true p (make_body t))
     else
       fun t p ->
-        let initunivs = Evd.evar_context_universe_context universes in
-	  Future.from_val (initunivs, nf t), 
-	  Future.chain ~pure:true p (fun (pt,eff) ->
-	    (pt, Evd.evar_universe_context_set (Future.force univs)), eff)
+        let initunivs = Evd.evar_context_universe_context initial_euctx in
+        Future.from_val (initunivs, nf t),
+        Future.chain ~pure:true p (fun (pt,eff) ->
+          (pt,Evd.evar_universe_context_set initunivs (Future.force univs)),eff)
   in
   let entries =
     Future.map2 (fun p (_, t) ->
@@ -336,15 +366,11 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl =
   { id = pid; entries = entries; persistence = strength; universes = universes },
   fun pr_ending -> Ephemeron.get terminator pr_ending
 
-type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context
+type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
 
 let return_proof ?(allow_partial=false) () =
  let { pid; proof; strength = (_,poly,_) } = cur_pstate () in
  if allow_partial then begin
-  if Proof.is_done proof then begin
-    msg_warning (str"The proof of " ++ str (Names.Id.to_string pid) ++
-     str" is complete, no need to end it with Admitted");
-  end;
   let proofs = Proof.partial_proof proof in
   let _,_,_,_, evd = Proof.proof proof in
   let eff = Evd.eval_side_effects evd in
@@ -370,10 +396,7 @@ let return_proof ?(allow_partial=false) () =
     | Proof.HasUnresolvedEvar->
         error(strbrk"Attempt to save a proof with existential variables still non-instantiated") in
   let eff = Evd.eval_side_effects evd in
-  let evd =
-    if poly || !Flags.compilation_mode = Flags.BuildVo
-    then Evd.nf_constraints evd
-    else evd in
+  let evd = Evd.nf_constraints evd in
   (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
       side-effects... This may explain why one need to uniquize side-effects
       thereafter... *)
@@ -382,9 +405,9 @@ let return_proof ?(allow_partial=false) () =
     proofs, Evd.evar_universe_context evd
 
 let close_future_proof ~feedback_id proof =
-  close_proof ~keep_body_ucst_sepatate:true ~feedback_id ~now:false proof
-let close_proof ~keep_body_ucst_sepatate fix_exn =
-  close_proof ~keep_body_ucst_sepatate ~now:true
+  close_proof ~keep_body_ucst_separate:true ~feedback_id ~now:false proof
+let close_proof ~keep_body_ucst_separate fix_exn =
+  close_proof ~keep_body_ucst_separate ~now:true
     (Future.from_val ~fix_exn (return_proof ()))
 
 (** Gets the current terminator without checking that the proof has
@@ -668,4 +691,13 @@ let freeze ~marshallable =
   | `No -> !pstates
 let unfreeze s = pstates := s; update_proof_mode ()
 let proof_of_state = function { proof }::_ -> proof | _ -> raise NoCurrentProof
-
+let copy_terminators ~src ~tgt =
+  assert(List.length src = List.length tgt);
+  List.map2 (fun op p -> { p with terminator = op.terminator }) src tgt
+
+let update_global_env () =
+  with_current_proof (fun _ p ->
+     Proof.in_proof p (fun sigma ->
+       let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in
+       let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac p in
+         (p, ())))