diff options
36 files changed, 233 insertions, 44 deletions
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index c781c8274..e5dc669dd 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -133,6 +133,24 @@ one gulp, as a proof term (see Section~\ref{exact}). \SeeAlso {\tt Proof with {\tac}.} in Section~\ref{ProofWith}. +\subsection[\tt Proof using {\ident$_1$ \dots {\ident$_n$}}.] +{\tt Proof using {\ident$_1$ \dots {\ident$_n$}}. +\comindex{Proof using} \label{ProofUsing}} + +This command applies in proof editing mode. +It declares the set of section variables (see~\ref{Variable}) +used by the proof. At {\tt Qed} time, the system will assert that +the set of section variables actually used in the proof is a subset of +the declared one. + +The set of declared variables is closed under type dependency. +For example if {\tt T} is variable and {\tt a} is a variable of +type {\tt T}, the commands {\tt Proof using a} and +{\tt Proof using T a} are actually equivalent. + +\variant {\tt Proof using {\ident$_1$ \dots {\ident$_n$}} with {\tac}.} +in Section~\ref{ProofWith}. + \subsection[\tt Abort.]{\tt Abort.\comindex{Abort}} This command cancels the current proof development, switching back to diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index d0c193de1..198f8f304 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -4239,6 +4239,16 @@ e.g. \texttt{Require Import A.}). \SeeAlso {\tt Proof.} in Section~\ref{BeginProof}. +\begin{Variants} +\item {\tt Proof with {\tac} using {\ident$_1$ \dots {\ident$_n$}}} + Combines in a single line {\tt Proof with} and {\tt Proof using}, + see~\ref{ProofUsing} +\item {\tt Proof using {\ident$_1$ \dots {\ident$_n$}} with {\tac}} + Combines in a single line {\tt Proof with} and {\tt Proof using}, + see~\ref{ProofUsing} + +\end{Variants} + \subsubsection[\tt Declare Implicit Tactic {\tac}.]{\tt Declare Implicit Tactic {\tac}.\comindex{Declare Implicit Tactic}} This command declares a tactic to be used to solve implicit arguments diff --git a/kernel/entries.ml b/kernel/entries.ml index 28f11c9af..a4485fac7 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -56,12 +56,13 @@ type mutual_inductive_entry = { type definition_entry = { const_entry_body : constr; + const_entry_secctx : section_context option; const_entry_type : types option; const_entry_opaque : bool } type inline = int option (* inlining level, None for no inlining *) -type parameter_entry = types * inline +type parameter_entry = section_context option * types * inline type constant_entry = | DefinitionEntry of definition_entry diff --git a/kernel/entries.mli b/kernel/entries.mli index 08740afae..b726d0ec0 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -52,12 +52,13 @@ type mutual_inductive_entry = { type definition_entry = { const_entry_body : constr; + const_entry_secctx : section_context option; const_entry_type : types option; const_entry_opaque : bool } type inline = int option (* inlining level, None for no inlining *) -type parameter_entry = types * inline +type parameter_entry = section_context option * types * inline type constant_entry = | DefinitionEntry of definition_entry diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index cc9366c11..478b9c6fc 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -102,11 +102,11 @@ let infer_declaration env dcl = then OpaqueDef (Declarations.opaque_from_val j.uj_val) else Def (Declarations.from_val j.uj_val) in - def, typ, cst - | ParameterEntry (t,nl) -> + def, typ, cst, c.const_entry_secctx + | ParameterEntry (ctx,t,nl) -> let (j,cst) = infer env t in let t = hcons_constr (Typeops.assumption_of_judgment env j) in - Undef nl, NonPolymorphicType t, cst + Undef nl, NonPolymorphicType t, cst, ctx let global_vars_set_constant_type env = function | NonPolymorphicType t -> global_vars_set env t @@ -116,14 +116,26 @@ let global_vars_set_constant_type env = function (fun t c -> Idset.union (global_vars_set env t) c)) ctx ~init:Idset.empty -let build_constant_declaration env kn (def,typ,cst) = - let ids_typ = global_vars_set_constant_type env typ in - let ids_def = match def with - | Undef _ -> Idset.empty - | Def cs -> global_vars_set env (Declarations.force cs) - | OpaqueDef lc -> global_vars_set env (Declarations.force_opaque lc) - in - let hyps = keep_hyps env (Idset.union ids_typ ids_def) in +let build_constant_declaration env kn (def,typ,cst,ctx) = + let hyps = + let inferred = + let ids_typ = global_vars_set_constant_type env typ in + let ids_def = match def with + | Undef _ -> Idset.empty + | Def cs -> global_vars_set env (Declarations.force cs) + | OpaqueDef lc -> + global_vars_set env (Declarations.force_opaque lc) in + keep_hyps env (Idset.union ids_typ ids_def) in + let declared = match ctx with + | None -> inferred + | Some declared -> declared in + let mk_set l = List.fold_right Idset.add (List.map pi1 l) Idset.empty in + let inferred_set, declared_set = mk_set inferred, mk_set declared in + if not (Idset.subset inferred_set declared_set) then + error ("The following section variable are used but not declared:\n"^ + (String.concat ", " (List.map string_of_id + (Idset.elements (Idset.diff inferred_set declared_set))))); + declared in let tps = Cemitcodes.from_val (compile_constant_body env def) in { const_hyps = hyps; const_body = def; @@ -137,7 +149,8 @@ let translate_constant env kn ce = build_constant_declaration env kn (infer_declaration env ce) let translate_recipe env kn r = - build_constant_declaration env kn (Cooking.cook_constant env r) + build_constant_declaration env kn + (let def,typ,cst = Cooking.cook_constant env r in def,typ,cst,None) (* Insertion of inductive types. *) diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 158f2c787..3bbf56677 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -22,10 +22,11 @@ val translate_local_assum : env -> types -> types * Univ.constraints val infer_declaration : env -> constant_entry -> - constant_def * constant_type * constraints + constant_def * constant_type * constraints * Sign.section_context option val build_constant_declaration : env -> 'a -> - constant_def * constant_type * constraints -> constant_body + constant_def * constant_type * constraints * Sign.section_context option -> + constant_body val translate_constant : env -> constant -> constant_entry -> constant_body diff --git a/library/declare.ml b/library/declare.ml index 0afd4bd9e..288580850 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -148,7 +148,7 @@ let discharge_constant ((sp,kn),(cdt,dhyps,kind)) = Some (GlobalRecipe recipe,(discharged_hyps kn sechyps)@dhyps,kind) (* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_constant_entry = ConstantEntry (ParameterEntry (mkProp,None)) +let dummy_constant_entry = ConstantEntry (ParameterEntry (None,mkProp,None)) let dummy_constant (ce,_,mk) = dummy_constant_entry,[],mk diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 0f5d80a83..78299448a 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -34,9 +34,15 @@ GEXTEND Gram ; command: [ [ IDENT "Goal"; c = lconstr -> VernacGoal c - | IDENT "Proof" -> VernacProof (Tacexpr.TacId []) - | IDENT "Proof"; "with"; ta = tactic -> VernacProof ta + | IDENT "Proof" -> VernacProof (None,None) | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn + | IDENT "Proof"; "with"; ta = tactic; + l = OPT [ "using"; l = LIST0 identref -> l ] -> + VernacProof (Some ta, l) + | IDENT "Proof"; "using"; l = LIST0 identref; + ta = OPT [ "with"; ta = tactic -> ta ] -> + VernacProof (ta,Some l) + | IDENT "Proof"; c = lconstr -> VernacExactProof c | IDENT "Abort" -> VernacAbort None | IDENT "Abort"; IDENT "All" -> VernacAbortAll | IDENT "Abort"; id = identref -> VernacAbort (Some id) @@ -56,7 +62,6 @@ GEXTEND Gram | IDENT "Resume" -> VernacResume None | IDENT "Resume"; id = identref -> VernacResume (Some id) | IDENT "Restart" -> VernacRestart - | IDENT "Proof"; c = lconstr -> VernacExactProof c | IDENT "Undo" -> VernacUndo 1 | IDENT "Undo"; n = natural -> VernacUndo n | IDENT "Undo"; IDENT "To"; n = natural -> VernacUndoTo n diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 27de53cad..e10d42b9d 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -972,9 +972,12 @@ let rec pr_vernac = function (* For extension *) | VernacExtend (s,c) -> pr_extend s c - | VernacProof (Tacexpr.TacId _) -> str "Proof" - | VernacProof te -> str "Proof with" ++ spc() ++ pr_raw_tactic te - + | VernacProof (None, None) -> str "Proof" + | VernacProof (None, Some l) -> str "Proof using" ++spc()++ prlist pr_lident l + | VernacProof (Some te, None) -> str "Proof with" ++ spc() ++ pr_raw_tactic te + | VernacProof (Some te, Some l) -> + str "Proof using" ++spc()++ prlist pr_lident l ++ spc() ++ + str "with" ++ spc() ++pr_raw_tactic te | VernacProofMode s -> str ("Proof Mode "^s) | VernacSubproof None -> str "BeginSubproof" | VernacSubproof (Some i) -> str "BeginSubproof " ++ pr_int i diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index f37cb3ed0..6df9d574f 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -381,6 +381,7 @@ let generate_functional_principle (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) let ce = { const_entry_body = value; + const_entry_secctx = None; const_entry_type = None; const_entry_opaque = false } in diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 233cdddd7..dd475315c 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -158,6 +158,7 @@ let definition_message id = let save with_clean id const (locality,kind) hook = let {const_entry_body = pft; + const_entry_secctx = _; const_entry_type = tpo; const_entry_opaque = opacity } = const in let l,r = match locality with diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index c65d3181c..55ebd31b9 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1131,6 +1131,7 @@ let (value_f:constr list -> global_reference -> constr) = let (declare_fun : identifier -> logical_kind -> constr -> global_reference) = fun f_id kind value -> let ce = {const_entry_body = value; + const_entry_secctx = None; const_entry_type = None; const_entry_opaque = false } in ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index d189a4e55..9d61c06de 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -158,6 +158,7 @@ let ty c = Typing.type_of (Global.env()) Evd.empty c let decl_constant na c = mkConst(declare_constant (id_of_string na) (DefinitionEntry { const_entry_body = c; + const_entry_secctx = None; const_entry_type = None; const_entry_opaque = true }, IsProof Lemma)) diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml index f02e83ad1..ecae6759f 100644 --- a/plugins/subtac/subtac_command.ml +++ b/plugins/subtac/subtac_command.ml @@ -325,7 +325,8 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = let body = it_mkLambda_or_LetIn (mkApp (constr_of_global gr, [|make|])) binders_rel in let ty = it_mkProd_or_LetIn top_arity binders_rel in let ce = - { const_entry_body = Evarutil.nf_evar !isevars body; + { const_entry_body = Evarutil.nf_evar !isevars body; + const_entry_secctx = None; const_entry_type = Some ty; const_entry_opaque = false } in diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index a719a9f9a..64d9f72ca 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -248,6 +248,7 @@ let declare_definition prg = let (local, kind) = prg.prg_kind in let ce = { const_entry_body = body; + const_entry_secctx = None; const_entry_type = Some typ; const_entry_opaque = false } in @@ -347,6 +348,7 @@ let declare_obligation prg obl body = let opaque = if get_proofs_transparency () then false else opaque in let ce = { const_entry_body = body; + const_entry_secctx = None; const_entry_type = Some ty; const_entry_opaque = opaque } in @@ -661,8 +663,8 @@ let admit_obligations n = match x.obl_body with | None -> let x = subst_deps_obl obls x in - let kn = Declare.declare_constant x.obl_name (ParameterEntry (x.obl_type,None), - IsAssumption Conjectural) + let kn = Declare.declare_constant x.obl_name + (ParameterEntry (None, x.obl_type,None), IsAssumption Conjectural) in assumption_message x.obl_name; obls.(i) <- { x with obl_body = Some (mkConst kn) } diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index e67c595bd..3d507f358 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -91,6 +91,11 @@ let set_end_tac tac = let tac = Proofview.V82.tactic tac in Proof_global.set_endline_tactic tac +let set_used_variables l = + Proof_global.set_used_variables l +let get_used_variables () = + Proof_global.get_used_variables () + exception NoSuchGoal let _ = Errors.register_handler begin function | NoSuchGoal -> Util.error "No such goal." diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 289e8c13c..7297b975f 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -154,6 +154,12 @@ val get_all_proof_names : unit -> identifier list val set_end_tac : tactic -> unit (** {6 ... } *) +(** [set_used_variables l] declares that section variables [l] will be + used in the proof *) +val set_used_variables : identifier list -> unit +val get_used_variables : unit -> Sign.section_context option + +(** {6 ... } *) (** [solve_nth n tac] applies tactic [tac] to the [n]th subgoal of the current focused proof or raises a UserError if no proof is focused or if there is no [n]th subgoal *) diff --git a/proofs/proof.ml b/proofs/proof.ml index 2aa31cd25..72730495d 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -119,6 +119,7 @@ type proof_state = { type proof_info = { mutable endline_tactic : unit Proofview.tactic ; + mutable section_vars : Sign.section_context option; initial_conclusions : Term.types list } @@ -219,6 +220,11 @@ let _unfocus pr = pr.state <- { pr.state with proofview = Proofview.unfocus fc pr.state.proofview } +let set_used_variables l p = + p.info.section_vars <- Some l + +let get_used_variables p = p.info.section_vars + (*** Endline tactic ***) (* spiwack this is an information about the UI, it might be a good idea to move @@ -364,7 +370,8 @@ let start goals = undo_stack = [] ; transactions = [] ; info = { endline_tactic = Proofview.tclUNIT (); - initial_conclusions = List.map snd goals } + initial_conclusions = List.map snd goals; + section_vars = None } } in _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr; diff --git a/proofs/proof.mli b/proofs/proof.mli index d80ac79af..12af18f40 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -129,6 +129,9 @@ val get_proof_info : proof -> Store.t val set_proof_info : Store.t -> proof -> unit +(* Sets the section variables assumed by the proof *) +val set_used_variables : Sign.section_context -> proof -> unit +val get_used_variables : proof -> Sign.section_context option (*** Endline tactic ***) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index e9af46ba9..2745270a6 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -267,6 +267,16 @@ let set_endline_tactic tac = let p = give_me_the_proof () in Proof.set_endline_tactic tac p +let set_used_variables l = + let p = give_me_the_proof () in + let env = Global.env () in + let ids = List.fold_right Idset.add l Idset.empty in + let ctx = Environ.keep_hyps env ids in + Proof.set_used_variables ctx p + +let get_used_variables () = + Proof.get_used_variables (give_me_the_proof ()) + let with_end_tac tac = let p = give_me_the_proof () in Proof.with_end_tac p tac @@ -278,9 +288,11 @@ let close_proof () = let id = get_current_proof_name () in let p = give_me_the_proof () in let proofs_and_types = Proof.return p in + let section_vars = Proof.get_used_variables p in let entries = List.map - (fun (c,t) -> { Entries.const_entry_body = c ; - const_entry_type = Some t; + (fun (c,t) -> { Entries.const_entry_body = c; + const_entry_secctx = section_vars; + const_entry_type = Some t; const_entry_opaque = true }) proofs_and_types in diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 2f9f4a549..ed6a60c71 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -82,6 +82,10 @@ val run_tactic : unit Proofview.tactic -> unit (** Sets the tactic to be used when a tactic line is closed with [...] *) val set_endline_tactic : unit Proofview.tactic -> unit +(** Sets the section variables assumed by the proof *) +val set_used_variables : Names.identifier list -> unit +val get_used_variables : unit -> Sign.section_context option + (** Appends the endline tactic of the current proof to a tactic. *) val with_end_tac : unit Proofview.tactic -> unit Proofview.tactic diff --git a/tactics/leminv.ml b/tactics/leminv.ml index a6915461d..1697c1465 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -235,6 +235,7 @@ let add_inversion_lemma name env sigma t sort dep inv_op = declare_constant name (DefinitionEntry { const_entry_body = invProof; + const_entry_secctx = None; const_entry_type = None; const_entry_opaque = false }, IsProof Lemma) diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 805f4260a..80930af42 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1647,6 +1647,7 @@ let declare_projection n instance_id r = let typ = it_mkProd_or_LetIn typ ctx in let cst = { const_entry_body = term; + const_entry_secctx = None; const_entry_type = Some typ; const_entry_opaque = false } in @@ -1713,7 +1714,7 @@ let add_morphism_infer glob m n = let instance = build_morphism_signature m in if Lib.is_modtype () then let cst = Declare.declare_constant ~internal:Declare.KernelSilent instance_id - (Entries.ParameterEntry (instance,None), Decl_kinds.IsAssumption Decl_kinds.Logical) + (Entries.ParameterEntry (None,instance,None), Decl_kinds.IsAssumption Decl_kinds.Logical) in add_instance (Typeclasses.new_instance (Lazy.force proper_class) None glob (ConstRef cst)); declare_projection n instance_id (ConstRef cst) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 25a148bbd..45eee91ee 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3516,7 +3516,8 @@ let admit_as_an_axiom gl = let concl = it_mkNamedProd_or_LetIn (pf_concl gl) sign in if occur_existential concl then error"\"admit\" cannot handle existentials."; let axiom = - let cd = Entries.ParameterEntry (concl,None) in + let cd = + Entries.ParameterEntry (Pfedit.get_used_variables(),concl,None) in let con = Declare.declare_constant ~internal:Declare.KernelSilent na (cd,IsAssumption Logical) in constr_of_global (ConstRef con) in diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v new file mode 100644 index 000000000..93a9ef116 --- /dev/null +++ b/test-suite/success/proof_using.v @@ -0,0 +1,61 @@ +Section Foo. + +Variable a : nat. + +Lemma l1 : True. +Fail Proof using non_existing. +Proof using a. +exact I. +Qed. + +Lemma l2 : True. +Proof using a. +Admitted. + +Lemma l3 : True. +Proof using a. +admit. +Qed. + +End Foo. + +Check (l1 3). +Check (l2 3). +Check (l3 3). + +Section Bar. + +Variable T : Type. +Variable a b : T. +Variable H : a = b. + +Lemma l4 : a = b. +Proof using H. +exact H. +Qed. + +End Bar. + +Check (l4 _ 1 1 _ : 1 = 1). + +Section S1. + +Variable v1 : nat. + +Section S2. + +Variable v2 : nat. + +Lemma deep : v1 = v2. +Proof using v1 v2. +admit. +Qed. + +End S2. + +Check (deep 3 : v1 = 3). + +End S1. + +Check (deep 3 4 : 3 = 4). + 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 |