aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/autoinstance.ml8
-rw-r--r--toplevel/class.ml1
-rw-r--r--toplevel/classes.ml6
-rw-r--r--toplevel/command.ml10
-rw-r--r--toplevel/ide_slave.ml2
-rw-r--r--toplevel/ind_tables.ml1
-rw-r--r--toplevel/indschemes.ml1
-rw-r--r--toplevel/lemmas.ml6
-rw-r--r--toplevel/record.ml3
-rw-r--r--toplevel/vernacentries.ml15
-rw-r--r--toplevel/vernacexpr.ml2
11 files changed, 42 insertions, 13 deletions
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index 79ae41c1d..9258a39fc 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.ml
@@ -179,7 +179,8 @@ let declare_record_instance gr ctx params =
let ident = make_instance_ident gr in
let def = it_mkLambda_or_LetIn (applistc (constr_of_global gr) params) ctx in
let def = deep_refresh_universes def in
- let ce = { const_entry_body=def;
+ let ce = { const_entry_body= def;
+ const_entry_secctx = None;
const_entry_type=None;
const_entry_opaque=false } in
let cst = Declare.declare_constant ident
@@ -194,8 +195,9 @@ let declare_class_instance gr ctx params =
let def = deep_refresh_universes def in
let typ = deep_refresh_universes typ in
let ce = Entries.DefinitionEntry
- { const_entry_type=Some typ;
- const_entry_body=def;
+ { const_entry_type = Some typ;
+ const_entry_secctx = None;
+ const_entry_body= def;
const_entry_opaque=false } in
try
let cst = Declare.declare_constant ident
diff --git a/toplevel/class.ml b/toplevel/class.ml
index e977959d2..ebaa19b66 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -219,6 +219,7 @@ let build_id_coercion idf_opt source =
let constr_entry = (* Cast is necessary to express [val_f] is identity *)
DefinitionEntry
{ const_entry_body = mkCast (val_f, DEFAULTcast, typ_f);
+ const_entry_secctx = None;
const_entry_type = Some typ_f;
const_entry_opaque = false } in
let kn = declare_constant idf (constr_entry,IsDefinition IdentityCoercion) in
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 61d7d31d7..1e83e4b81 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -110,6 +110,7 @@ let declare_instance_constant k pri global imps ?hook id term termtype =
let kind = IsDefinition Instance in
let entry =
{ const_entry_body = term;
+ const_entry_secctx = None;
const_entry_type = Some termtype;
const_entry_opaque = false }
in DefinitionEntry entry, kind
@@ -182,7 +183,8 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
in
Evarutil.check_evars env Evd.empty !evars termtype;
let cst = Declare.declare_constant ~internal:Declare.KernelSilent id
- (Entries.ParameterEntry (termtype,None), Decl_kinds.IsAssumption Decl_kinds.Logical)
+ (Entries.ParameterEntry
+ (None,termtype,None), Decl_kinds.IsAssumption Decl_kinds.Logical)
in instance_hook k None global imps ?hook (ConstRef cst); id
end
else
@@ -297,7 +299,7 @@ let context l =
let fn (id, _, t) =
if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
let cst = Declare.declare_constant ~internal:Declare.KernelSilent id
- (ParameterEntry (t,None), IsAssumption Logical)
+ (ParameterEntry (None,t,None), IsAssumption Logical)
in
match class_of_constr t with
| Some (rels, (tc, args) as _cl) ->
diff --git a/toplevel/command.ml b/toplevel/command.ml
index fff6eb6fa..ffb1130eb 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -62,7 +62,7 @@ let red_constant_entry n ce = function
| Some red ->
let body = ce.const_entry_body in
{ ce with const_entry_body =
- under_binders (Global.env()) (fst (reduction_of_red_expr red)) n body }
+ under_binders (Global.env()) (fst (reduction_of_red_expr red)) n body }
let interp_definition bl red_option c ctypopt =
let env = Global.env() in
@@ -77,6 +77,7 @@ let interp_definition bl red_option c ctypopt =
check_evars env Evd.empty !evdref body;
imps1@(Impargs.lift_implicits nb_args imps2),
{ const_entry_body = body;
+ const_entry_secctx = None;
const_entry_type = None;
const_entry_opaque = false }
| Some ctyp ->
@@ -88,6 +89,7 @@ let interp_definition bl red_option c ctypopt =
check_evars env Evd.empty !evdref typ;
imps1@(Impargs.lift_implicits nb_args imps2),
{ const_entry_body = body;
+ const_entry_secctx = None;
const_entry_type = Some typ;
const_entry_opaque = false }
in
@@ -112,7 +114,7 @@ let declare_definition ident (local,k) ce imps hook =
let r = match local with
| Local when Lib.sections_are_opened () ->
let c =
- SectionLocalDef(ce.const_entry_body,ce.const_entry_type,false) in
+ SectionLocalDef(ce.const_entry_body ,ce.const_entry_type,false) in
let _ = declare_variable ident (Lib.cwd(),c,IsDefinition k) in
definition_message ident;
if Pfedit.refining () then
@@ -140,7 +142,8 @@ let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) =
Typeclasses.declare_instance None true r; r
| (Global|Local) ->
let kn =
- declare_constant ident (ParameterEntry (c,nl), IsAssumption kind) in
+ declare_constant ident
+ (ParameterEntry (None,c,nl), IsAssumption kind) in
let gr = ConstRef kn in
maybe_declare_manual_implicits false gr imps;
assumption_message ident;
@@ -474,6 +477,7 @@ let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
let declare_fix kind f def t imps =
let ce = {
const_entry_body = def;
+ const_entry_secctx = None;
const_entry_type = Some t;
const_entry_opaque = false }
in
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 9d0f17ee7..e43a23c95 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -204,7 +204,7 @@ let rec attribute_of_vernac_command = function
| VernacUnfocus -> [SolveCommand]
| VernacShow _ -> [OtherStatePreservingCommand]
| VernacCheckGuard -> [OtherStatePreservingCommand]
- | VernacProof (Tacexpr.TacId []) -> [OtherStatePreservingCommand]
+ | VernacProof (None, None) -> [OtherStatePreservingCommand]
| VernacProof _ -> []
| VernacProofMode _ -> []
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 30c537f28..de3b62f82 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -125,6 +125,7 @@ let define internal id c =
let kn = fd id
(DefinitionEntry
{ const_entry_body = c;
+ const_entry_secctx = None;
const_entry_type = None;
const_entry_opaque = false },
Decl_kinds.IsDefinition Scheme) in
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index e3779e131..d346f422e 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -110,6 +110,7 @@ let define id internal c t =
let kn = f id
(DefinitionEntry
{ const_entry_body = c;
+ const_entry_secctx = None;
const_entry_type = t;
const_entry_opaque = false },
Decl_kinds.IsDefinition Scheme) in
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 5817ef1b9..6f344db58 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -199,7 +199,7 @@ let save_remaining_recthms (local,kind) body opaq i (id,(t_i,(_,imps))) =
(Local,VarRef id,imps)
| Global ->
let k = IsAssumption Conjectural in
- let kn = declare_constant id (ParameterEntry (t_i,None), k) in
+ let kn = declare_constant id (ParameterEntry (None,t_i,None), k) in
(Global,ConstRef kn,imps))
| Some body ->
let k = logical_kind_of_goal_kind kind in
@@ -215,6 +215,7 @@ let save_remaining_recthms (local,kind) body opaq i (id,(t_i,(_,imps))) =
| Global ->
let const =
{ const_entry_body = body_i;
+ const_entry_secctx = None;
const_entry_type = Some t_i;
const_entry_opaque = opaq } in
let kn = declare_constant id (DefinitionEntry const, k) in
@@ -328,8 +329,9 @@ let start_proof_com kind thms hook =
let admit () =
let (id,k,typ,hook) = Pfedit.current_proof_statement () in
+ let e = Pfedit.get_used_variables(), typ, None in
let kn =
- declare_constant id (ParameterEntry (typ,None),IsAssumption Conjectural) in
+ declare_constant id (ParameterEntry e,IsAssumption Conjectural) in
Pfedit.delete_current_proof ();
assumption_message id;
hook Global (ConstRef kn)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index ee190d350..86849cbbb 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -203,6 +203,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
try
let cie = {
const_entry_body = proj;
+ const_entry_secctx = None;
const_entry_type = Some projtyp;
const_entry_opaque = false } in
let k = (DefinitionEntry cie,IsDefinition kind) in
@@ -312,6 +313,7 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
let class_type = Option.map (fun ar -> it_mkProd_or_LetIn ar params) arity in
let class_entry =
{ const_entry_body = class_body;
+ const_entry_secctx = None;
const_entry_type = class_type;
const_entry_opaque = false }
in
@@ -323,6 +325,7 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
let proj_body = it_mkLambda_or_LetIn (mkLambda (Name (snd id), inst_type, mkRel 1)) params in
let proj_entry =
{ const_entry_body = proj_body;
+ const_entry_secctx = None;
const_entry_type = Some proj_type;
const_entry_opaque = false }
in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 110e6190c..435d85233 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -674,6 +674,15 @@ let vernac_set_end_tac tac =
if tac <> (Tacexpr.TacId []) then set_end_tac (Tacinterp.interp tac) else ()
(* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
+let vernac_set_used_variables l =
+ let l = List.map snd l in
+ if not (list_distinct l) then error "Used variables list contains duplicates";
+ let vars = Environ.named_context (Global.env ()) in
+ List.iter (fun id ->
+ if not (List.exists (fun (id',_,_) -> id = id') vars) then
+ error ("Unknown variable: " ^ string_of_id id))
+ l;
+ set_used_variables l
(*****************************)
(* Auxiliary file management *)
@@ -1514,7 +1523,11 @@ let interp c = match c with
| VernacEndSubproof -> vernac_end_subproof ()
| VernacShow s -> vernac_show s
| VernacCheckGuard -> vernac_check_guard ()
- | VernacProof tac -> vernac_set_end_tac tac
+ | VernacProof (None, None) -> ()
+ | VernacProof (Some tac, None) -> vernac_set_end_tac tac
+ | VernacProof (None, Some l) -> vernac_set_used_variables l
+ | VernacProof (Some tac, Some l) ->
+ vernac_set_end_tac tac; vernac_set_used_variables l
| VernacProofMode mn -> Proof_global.set_proof_mode mn
(* Toplevel control *)
| VernacToplevelControl e -> raise e
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 33a474923..b1ab3bdce 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -357,7 +357,7 @@ type vernac_expr =
| VernacEndSubproof
| VernacShow of showable
| VernacCheckGuard
- | VernacProof of raw_tactic_expr
+ | VernacProof of raw_tactic_expr option * lident list option
| VernacProofMode of string
(* Toplevel control *)
| VernacToplevelControl of exn
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 07:02:56 +0000