From 164c6861860e6b52818c031f901ffeff91fca16a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 26 Jan 2016 16:56:33 +0100 Subject: Imported Upstream version 8.5 --- stm/lemmas.ml | 65 +++++++++++++++++++++++++++++++---------------------------- 1 file changed, 34 insertions(+), 31 deletions(-) (limited to 'stm/lemmas.ml') diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 6c183268..f06abfcc 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* exn) hook l r with e when Errors.noncritical e -> let e = Errors.push e in @@ -219,11 +220,11 @@ let compute_proof_name locality = function locality == Global && Nametab.exists_cci (Lib.make_path_except_section id) then user_err_loc (loc,"",pr_id id ++ str " already exists."); - id + id, pl | None -> - next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()) + next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()), None -let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,imps))) = +let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,(_,imps))) = let t_i = norm t_i in match body with | None -> @@ -276,28 +277,28 @@ let save_hook = ref ignore let set_save_hook f = save_hook := f let save_named ?export_seff proof = - let id,const,cstrs,do_guard,persistence,hook = proof in - save ?export_seff id const cstrs do_guard persistence hook + let id,const,(cstrs,pl),do_guard,persistence,hook = proof in + save ?export_seff id const cstrs pl 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 ?export_seff proof save_ident = - let id,const,cstrs,do_guard,persistence,hook = proof in + let id,const,(cstrs,pl),do_guard,persistence,hook = proof in check_anonymity id save_ident; - save ?export_seff save_ident const cstrs do_guard persistence hook + save ?export_seff save_ident const cstrs pl do_guard persistence hook let save_anonymous_with_strength ?export_seff proof kind save_ident = - let id,const,cstrs,do_guard,_,hook = proof in + let id,const,(cstrs,pl),do_guard,_,hook = proof in check_anonymity id save_ident; (* we consider that non opaque behaves as local for discharge *) - save ?export_seff save_ident const cstrs do_guard (Global, const.const_entry_polymorphic, Proof kind) hook + save ?export_seff save_ident const cstrs pl do_guard + (Global, const.const_entry_polymorphic, Proof kind) hook (* Admitted *) -let admit (id,k,e) hook () = +let admit (id,k,e) pl hook () = let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in let () = match k with | Global, _, _ -> () @@ -306,6 +307,7 @@ let admit (id,k,e) hook () = str "declared as an axiom.") in let () = assumption_message id in + Option.iter (Universes.register_universe_binders (ConstRef kn)) pl; call_hook (fun exn -> exn) hook Global (ConstRef kn) (* Starting a goal *) @@ -315,11 +317,10 @@ let set_start_hook = (:=) start_hook let get_proof proof do_guard hook opacity = - let (id,(const,cstrs,persistence)) = + let (id,(const,univs,persistence)) = Pfedit.cook_this_proof proof in - (** FIXME *) - id,{const with const_entry_opaque = opacity},cstrs,do_guard,persistence,hook + id,{const with const_entry_opaque = opacity},univs,do_guard,persistence,hook let check_exist = List.iter (fun (loc,id) -> @@ -329,16 +330,16 @@ let check_exist = let universe_proof_terminator compute_guard hook = let open Proof_global in function - | Admitted (id,k,pe,ctx) -> - admit (id,k,pe) (hook (Some ctx)) (); + | Admitted (id,k,pe,(ctx,pl)) -> + admit (id,k,pe) pl (hook (Some ctx)) (); 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 (Some proof.Proof_global.universes)) is_opaque in + let proof = get_proof proof compute_guard + (hook (Some (fst proof.Proof_global.universes))) is_opaque in begin match idopt with | None -> save_named ~export_seff proof | Some ((_,id),None) -> save_anonymous ~export_seff proof id @@ -350,7 +351,7 @@ let universe_proof_terminator compute_guard hook = 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 start_proof id ?pl kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook = let terminator = standard_proof_terminator compute_guard hook in let sign = match sign with @@ -358,9 +359,9 @@ let start_proof id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook = | None -> initialize_named_context_for_proof () in !start_hook c; - Pfedit.start_proof id kind sigma sign c ?init_tac terminator + Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator -let start_proof_univs id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook = +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 sign = match sign with @@ -368,11 +369,11 @@ let start_proof_univs id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook = | None -> initialize_named_context_for_proof () in !start_hook c; - Pfedit.start_proof id kind sigma sign c ?init_tac terminator + Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator let rec_tac_initializer finite guard thms snl = if finite then - match List.map (fun (id,(t,_)) -> (id,t)) thms with + match List.map (fun ((id,_),(t,_)) -> (id,t)) thms with | (id,_)::l -> Tactics.mutual_cofix id l 0 | _ -> assert false else @@ -380,7 +381,7 @@ let rec_tac_initializer finite guard thms snl = let nl = match snl with | None -> List.map succ (List.map List.last guard) | Some nl -> nl - in match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with + in match List.map2 (fun ((id,_),(t,_)) n -> (id,n,t)) thms nl with | (id,n,_)::l -> Tactics.mutual_fix id n l 0 | _ -> assert false @@ -409,7 +410,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook = (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in match thms with | [] -> anomaly (Pp.str "No proof to start") - | (id,(t,(_,imps)))::other_thms -> + | ((id,pl),(t,(_,imps)))::other_thms -> let hook ctx strength ref = let ctx = match ctx with | None -> Evd.empty_evar_universe_context @@ -428,7 +429,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook = List.iter (fun (strength,ref,imps) -> maybe_declare_manual_implicits false ref imps; call_hook (fun exn -> exn) hook strength ref) thms_data in - start_proof_univs id kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard + 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 env0 = Global.env () in @@ -472,14 +473,13 @@ let save_proof ?proof = function if const_entry_type = None then error "Admitted requires an explicit statement"; let typ = Option.get const_entry_type in - let ctx = Evd.evar_context_universe_context universes in + let ctx = Evd.evar_context_universe_context (fst universes) in Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None), universes) | None -> let id, k, typ = Pfedit.current_proof_statement () in (* This will warn if the proof is complete *) let pproofs, universes = Proof_global.return_proof ~allow_partial:true () in - let ctx = Evd.evar_context_universe_context universes in let sec_vars = match Pfedit.get_used_variables(), pproofs with | Some _ as x, _ -> x @@ -489,7 +489,10 @@ let save_proof ?proof = function let ids_def = Environ.global_vars_set env pproof in Some (Environ.keep_hyps env (Idset.union ids_typ ids_def)) | _ -> None in - Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),universes) + let names = Pfedit.get_universe_binders () in + let binders, ctx = Evd.universe_context ?names (Evd.from_ctx universes) in + Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None), + (universes, Some binders)) in Proof_global.get_terminator() pe | Vernacexpr.Proved (is_opaque,idopt) -> -- cgit v1.2.3