Imported Upstream version 8.6upstream/8.6

1 files changed, 78 insertions, 38 deletions

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index f06abfcc..022c89ad 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -9,7 +9,7 @@
 (* Created by Hugo Herbelin from contents related to lemma proofs in
    file command.ml, Aug 2009 *)
 
-open Errors
+open CErrors
 open Util
 open Flags
 open Pp
@@ -31,20 +31,22 @@ open Reductionops
 open Constrexpr
 open Constrintern
 open Impargs
+open Context.Rel.Declaration
 
 type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference -> 'a
 let mk_hook hook = hook
 let call_hook fix_exn hook l c =
   try hook l c
-  with e when Errors.noncritical e ->
-    let e = Errors.push e in
+  with e when CErrors.noncritical e ->
+    let e = CErrors.push e in
     iraise (fix_exn e)
 
 (* Support for mutually proved theorems *)
 
 let retrieve_first_recthm = function
   | VarRef id ->
-      (pi2 (Global.lookup_named id),variable_opacity id)
+      let open Context.Named.Declaration in
+      (get_value (Global.lookup_named id),variable_opacity id)
   | ConstRef cst ->
       let cb = Global.lookup_constant cst in
       (Global.body_of_constant_body cb, is_opaque cb)
@@ -77,7 +79,7 @@ let adjust_guardness_conditions const = function
                     List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l)
                 env (Safe_typing.side_effects_of_private_constants eff) in
               let indexes =
-	        search_guard Loc.ghost env
+                search_guard Loc.ghost env
                   possible_indexes fixdecls in
 		(mkFix ((indexes,0),fixdecls), ctx), eff
           | _ -> (body, ctx), eff) }
@@ -104,20 +106,21 @@ let find_mutually_recursive_statements thms =
       (* Cofixpoint or fixpoint w/o explicit decreasing argument *)
       | None | Some (None, CStructRec) ->
       let whnf_hyp_hds = map_rel_context_in_env
-        (fun env c -> fst (whd_betadeltaiota_stack env Evd.empty c))
+        (fun env c -> fst (whd_all_stack env Evd.empty c))
         (Global.env()) hyps in
       let ind_hyps =
-        List.flatten (List.map_i (fun i (_,b,t) ->
+        List.flatten (List.map_i (fun i decl ->
+          let t = get_type decl in
           match kind_of_term t with
           | Ind ((kn,_ as ind),u) when
                 let mind = Global.lookup_mind kn in
-                mind.mind_finite <> Decl_kinds.CoFinite && Option.is_empty b ->
+                mind.mind_finite <> Decl_kinds.CoFinite && is_local_assum decl ->
               [ind,x,i]
           | _ ->
               []) 0 (List.rev whnf_hyp_hds)) in
       let ind_ccl =
         let cclenv = push_rel_context hyps (Global.env()) in
-        let whnf_ccl,_ = whd_betadeltaiota_stack cclenv Evd.empty ccl in
+        let whnf_ccl,_ = whd_all_stack cclenv Evd.empty ccl in
         match kind_of_term whnf_ccl with
         | Ind ((kn,_ as ind),u) when
               let mind = Global.lookup_mind kn in
@@ -147,7 +150,7 @@ let find_mutually_recursive_statements thms =
 	  assert (List.is_empty rest);
           (* One occ. of common coind ccls and no common inductive hyps *)
 	  if not (List.is_empty common_same_indhyp) then
-	    if_verbose msg_info (str "Assuming mutual coinductive statements.");
+	    if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements.");
 	  flush_all ();
           indccl, true, []
       | [], _::_ ->
@@ -155,7 +158,7 @@ let find_mutually_recursive_statements thms =
           | ind :: _ ->
             if List.distinct_f ind_ord (List.map pi1 ind)
             then
-              if_verbose msg_info
+              if_verbose Feedback.msg_info
                 (strbrk
                    ("Coinductive statements do not follow the order of "^
                     "definition, assuming the proof to be by induction."));
@@ -207,8 +210,8 @@ let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
     definition_message id;
     Option.iter (Universes.register_universe_binders r) pl;
     call_hook (fun exn -> exn) hook l r
-  with e when Errors.noncritical e ->
-    let e = Errors.push e in
+  with e when CErrors.noncritical e ->
+    let e = CErrors.push e in
     iraise (fix_exn e)
 
 let default_thm_id = Id.of_string "Unnamed_thm"
@@ -249,10 +252,14 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,
   | Some body ->
       let body = norm body in
       let k = Kindops.logical_kind_of_goal_kind kind in
-      let body_i = match kind_of_term body with
+      let rec body_i t = match kind_of_term t with
         | Fix ((nv,0),decls) -> mkFix ((nv,i),decls)
         | CoFix (0,decls) -> mkCoFix (i,decls)
+        | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2)
+        | Lambda(na,ty,t) -> mkLambda(na,ty,body_i t)
+        | App (t, args) -> mkApp (body_i t, args)
         | _ -> anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr body) in
+      let body_i = body_i body in
       match locality with
       | Discharge ->
           let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p 
@@ -298,13 +305,16 @@ let save_anonymous_with_strength ?export_seff proof kind save_ident =
 
 (* Admitted *)
 
+let warn_let_as_axiom =
+  CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
+                   (fun id -> strbrk "Let definition" ++ spc () ++ pr_id id ++
+                                spc () ++ strbrk "declared as an axiom.")
+
 let admit (id,k,e) pl hook () =
   let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in
   let () = match k with
   | Global, _, _ -> ()
-  | Local, _, _ | Discharge, _, _ ->
-    msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++
-      str "declared as an axiom.")
+  | Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id
   in
   let () = assumption_message id in
   Option.iter (Universes.register_universe_binders (ConstRef kn)) pl;
@@ -329,10 +339,11 @@ let check_exist =
   )
 
 let universe_proof_terminator compute_guard hook =
-  let open Proof_global in function
+  let open Proof_global in
+  make_terminator begin function
   | Admitted (id,k,pe,(ctx,pl)) ->
       admit (id,k,pe) pl (hook (Some ctx)) ();
-      Pp.feedback Feedback.AddedAxiom
+      Feedback.feedback Feedback.AddedAxiom
   | Proved (opaque,idopt,proof) ->
       let is_opaque, export_seff, exports = match opaque with
         | Vernacexpr.Transparent -> false, true, []
@@ -347,12 +358,16 @@ let universe_proof_terminator compute_guard hook =
           save_anonymous_with_strength ~export_seff proof kind id
       end;
       check_exist exports
+  end
 
 let standard_proof_terminator compute_guard hook =
   universe_proof_terminator compute_guard (fun _ -> hook)
 
-let start_proof id ?pl kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
-  let terminator = standard_proof_terminator compute_guard hook in
+let start_proof id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
+  let terminator = match terminator with
+  | None -> standard_proof_terminator compute_guard hook
+  | Some terminator -> terminator compute_guard hook
+  in
   let sign = 
     match sign with
     | Some sign -> sign
@@ -361,8 +376,11 @@ let start_proof id ?pl kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
   !start_hook c;
   Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator
 
-let start_proof_univs id ?pl kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
-  let terminator = universe_proof_terminator compute_guard hook in
+let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
+  let terminator = match terminator with
+  | None -> universe_proof_terminator compute_guard hook
+  | Some terminator -> terminator compute_guard hook
+  in
   let sign = 
     match sign with
     | Some sign -> sign
@@ -392,7 +410,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
     | Anonymous -> Tactics.intro) (List.rev ids) in
   let init_tac,guard = match recguard with
   | Some (finite,guard,init_tac) ->
-      let rec_tac = Proofview.V82.tactic (rec_tac_initializer finite guard thms snl) in
+      let rec_tac = rec_tac_initializer finite guard thms snl in
       Some (match init_tac with
         | None -> 
             if Flags.is_auto_intros () then 
@@ -422,7 +440,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
             let body,opaq = retrieve_first_recthm ref in
             let subst = Evd.evar_universe_context_subst ctx in
             let norm c = Universes.subst_opt_univs_constr subst c in
-	    let ctx = Evd.evar_universe_context_set (*FIXME*) Univ.UContext.empty ctx in
+	    let ctx = UState.context_set (*FIXME*) ctx in
 	    let body = Option.map norm body in
             List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in
         let thms_data = (strength,ref,imps)::other_thms_data in
@@ -431,7 +449,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
 	  call_hook (fun exn -> exn) hook strength ref) thms_data in
       start_proof_univs id ?pl kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
 
-let start_proof_com kind thms hook =
+let start_proof_com ?inference_hook kind thms hook =
   let env0 = Global.env () in
   let levels = Option.map snd (fst (List.hd thms)) in 
   let evdref = ref (match levels with
@@ -441,8 +459,10 @@ let start_proof_com kind thms hook =
   let thms = List.map (fun (sopt,(bl,t,guard)) ->
     let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
     let t', imps' = interp_type_evars_impls ~impls env evdref t in
-    evdref := solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref);
-    let ids = List.map pi1 ctx in
+    let flags = all_and_fail_flags in
+    let flags = { flags with use_hook = inference_hook } in
+    evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref);
+    let ids = List.map get_name ctx in
       (compute_proof_name (pi1 kind) sopt,
       (nf_evar !evdref (it_mkProd_or_LetIn t' ctx),
        (ids, imps @ lift_implicits (List.length ids) imps'),
@@ -451,6 +471,11 @@ let start_proof_com kind thms hook =
   let recguard,thms,snl = look_for_possibly_mutual_statements thms in
   let evd, nf = Evarutil.nf_evars_and_universes !evdref in
   let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in
+  let () =
+    match levels with
+    | None -> ()
+    | Some l -> ignore (Evd.universe_context evd ?names:l)
+  in
   let evd =
     if pi2 kind then evd
     else (* We fix the variables to ensure they won't be lowered to Set *)
@@ -461,6 +486,18 @@ let start_proof_com kind thms hook =
 
 (* Saving a proof *)
 
+let keep_admitted_vars = ref true
+
+let _ =
+  let open Goptions in
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "keep section variables in admitted proofs";
+      optkey   = ["Keep"; "Admitted"; "Variables"];
+      optread  = (fun () -> !keep_admitted_vars);
+      optwrite = (fun b -> keep_admitted_vars := b) }
+
 let save_proof ?proof = function
   | Vernacexpr.Admitted ->
       let pe =
@@ -474,14 +511,18 @@ let save_proof ?proof = function
               error "Admitted requires an explicit statement";
             let typ = Option.get const_entry_type in
             let ctx = Evd.evar_context_universe_context (fst universes) in
-            Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None), universes)
+            let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
+            Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes)
         | None ->
+            let pftree = Pfedit.get_pftreestate () in
             let id, k, typ = Pfedit.current_proof_statement () in
+            let universes = Proof.initial_euctx pftree in
             (* This will warn if the proof is complete *)
-            let pproofs, universes =
+            let pproofs, _univs =
               Proof_global.return_proof ~allow_partial:true () in
             let sec_vars =
-              match  Pfedit.get_used_variables(), pproofs with
+              if not !keep_admitted_vars then None
+              else match  Pfedit.get_used_variables(), pproofs with
               | Some _ as x, _ -> x
               | None, (pproof, _) :: _ -> 
                   let env = Global.env () in
@@ -490,11 +531,12 @@ let save_proof ?proof = function
                   Some (Environ.keep_hyps env (Idset.union ids_typ ids_def))
               | _ -> None in
 	    let names = Pfedit.get_universe_binders () in
-            let binders, ctx = Evd.universe_context ?names (Evd.from_ctx universes) in
+            let evd = Evd.from_ctx universes in
+            let binders, ctx = Evd.universe_context ?names evd in
             Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),
 		     (universes, Some binders))
       in
-      Proof_global.get_terminator() pe
+      Proof_global.apply_terminator (Proof_global.get_terminator ()) pe
   | Vernacexpr.Proved (is_opaque,idopt) ->
       let (proof_obj,terminator) =
         match proof with
@@ -504,12 +546,10 @@ let save_proof ?proof = function
       in
       (* if the proof is given explicitly, nothing has to be deleted *)
       if Option.is_empty proof then Pfedit.delete_current_proof ();
-      terminator (Proof_global.Proved (is_opaque,idopt,proof_obj))
+      Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj)))
 
 (* Miscellaneous *)
 
 let get_current_context () =
-  try Pfedit.get_current_goal_context ()
-  with e when Logic.catchable_exception e ->
-    let env = Global.env () in
-    (Evd.from_env env, env)
+  Pfedit.get_current_context ()
+