summaryrefslogtreecommitdiff
path: root/stm/lemmas.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
commit2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch)
tree074182834cb406d1304aec4233718564a9c06ba1 /stm/lemmas.ml
parent0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff)
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'stm/lemmas.ml')
-rw-r--r--stm/lemmas.ml67
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)