diff options
Diffstat (limited to 'stm/lemmas.ml')
| -rw-r--r-- | stm/lemmas.ml | 67 |
1 files changed, 30 insertions, 37 deletions
diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 6cece32e..6c183268 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -70,11 +70,12 @@ let adjust_guardness_conditions const = function try ignore(Environ.lookup_constant c e); true with Not_found -> false in if exists c e then e else Environ.add_constant c cb e in - let env = Declareops.fold_side_effects (fun env -> function + let env = List.fold_left (fun env { eff } -> + match eff with | SEsubproof (c, cb,_) -> add c cb env | SEscheme (l,_) -> List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l) - env (Declareops.uniquize_side_effects eff) in + env (Safe_typing.side_effects_of_private_constants eff) in let indexes = search_guard Loc.ghost env possible_indexes fixdecls in @@ -212,7 +213,7 @@ let save ?export_seff id const cstrs do_guard (locality,poly,kind) hook = let default_thm_id = Id.of_string "Unnamed_thm" let compute_proof_name locality = function - | Some (loc,id) -> + | Some ((loc,id),pl) -> (* We check existence here: it's a bit late at Qed time *) if Nametab.exists_cci (Lib.make_path id) || is_section_variable id || locality == Global && Nametab.exists_cci (Lib.make_path_except_section id) @@ -326,29 +327,10 @@ 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) -> - admit (id,k,pe) (hook None) (); + | Admitted (id,k,pe,ctx) -> + admit (id,k,pe) (hook (Some ctx)) (); Pp.feedback Feedback.AddedAxiom | Proved (opaque,idopt,proof) -> let is_opaque, export_seff, exports = match opaque with @@ -365,6 +347,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 = @@ -436,7 +421,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 ctx in + let ctx = Evd.evar_universe_context_set (*FIXME*) Univ.UContext.empty 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 @@ -447,11 +432,15 @@ let start_proof_with_initialization kind ctx recguard thms snl hook = let start_proof_com kind thms hook = let env0 = Global.env () in - let evdref = ref (Evd.from_env env0) in + let levels = Option.map snd (fst (List.hd thms)) in + let evdref = ref (match levels with + | None -> Evd.from_env env0 + | Some l -> Evd.from_ctx (Evd.make_evar_universe_context env0 l)) + in 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 - check_evars_are_solved env !evdref (Evd.empty,!evdref); + evdref := solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref); let ids = List.map pi1 ctx in (compute_proof_name (pi1 kind) sopt, (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), @@ -461,8 +450,12 @@ 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 - start_proof_with_initialization kind evd - recguard thms snl hook + let evd = + if pi2 kind then evd + else (* We fix the variables to ensure they won't be lowered to Set *) + Evd.fix_undefined_variables evd + in + start_proof_with_initialization kind evd recguard thms snl hook (* Saving a proof *) @@ -480,14 +473,13 @@ 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 universes in - Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None)) + Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None), universes) | None -> let id, k, typ = Pfedit.current_proof_statement () in - let ctx = - let evd, _ = Pfedit.get_current_goal_context () in - Evd.universe_context evd in (* This will warn if the proof is complete *) - let pproofs,_ = Proof_global.return_proof ~allow_partial:true () in + 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 @@ -497,14 +489,14 @@ 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)) + Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),universes) in Proof_global.get_terminator() pe | Vernacexpr.Proved (is_opaque,idopt) -> let (proof_obj,terminator) = match proof with | None -> - Proof_global.close_proof ~keep_body_ucst_sepatate:false (fun x -> x) + Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x) | Some proof -> proof in (* if the proof is given explicitly, nothing has to be deleted *) @@ -516,4 +508,5 @@ let save_proof ?proof = function let get_current_context () = try Pfedit.get_current_goal_context () with e when Logic.catchable_exception e -> - (Evd.empty, Global.env()) + let env = Global.env () in + (Evd.from_env env, env) |