summaryrefslogtreecommitdiff
path: root/stm/lemmas.ml
diff options
context:
space:
mode:
Diffstat (limited to 'stm/lemmas.ml')
-rw-r--r--stm/lemmas.ml65
1 files changed, 34 insertions, 31 deletions
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 *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -186,7 +186,7 @@ let look_for_possibly_mutual_statements = function
(* Saving a goal *)
-let save ?export_seff id const cstrs do_guard (locality,poly,kind) hook =
+let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
try
let const = adjust_guardness_conditions const do_guard in
@@ -205,6 +205,7 @@ let save ?export_seff id const cstrs do_guard (locality,poly,kind) hook =
declare_constant ?export_seff id ~local (DefinitionEntry const, k) in
(locality, ConstRef kn) in
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
@@ -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) ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 01:38:31 +0000