aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/attributes.ml8
-rw-r--r--vernac/attributes.mli1
-rw-r--r--vernac/auto_ind_decl.ml9
-rw-r--r--vernac/comDefinition.ml18
-rw-r--r--vernac/comDefinition.mli2
-rw-r--r--vernac/comFixpoint.ml23
-rw-r--r--vernac/comFixpoint.mli4
-rw-r--r--vernac/comProgramFixpoint.ml30
-rw-r--r--vernac/comProgramFixpoint.mli2
-rw-r--r--vernac/comTactic.ml6
-rw-r--r--vernac/comTactic.mli9
-rw-r--r--vernac/declare.ml172
-rw-r--r--vernac/declare.mli8
-rw-r--r--vernac/egramcoq.ml4
-rw-r--r--vernac/g_vernac.mlg95
-rw-r--r--vernac/himsg.ml4
-rw-r--r--vernac/indschemes.ml2
-rw-r--r--vernac/metasyntax.ml6
-rw-r--r--vernac/proof_using.ml26
-rw-r--r--vernac/proof_using.mli5
-rw-r--r--vernac/pvernac.ml3
-rw-r--r--vernac/pvernac.mli2
-rw-r--r--vernac/recLemmas.ml4
-rw-r--r--vernac/vernacentries.ml91
24 files changed, 306 insertions, 228 deletions
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index fb308fd316..efba6d332a 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -224,3 +224,11 @@ let canonical_field =
enable_attribute ~key:"canonical" ~default:(fun () -> true)
let canonical_instance =
enable_attribute ~key:"canonical" ~default:(fun () -> false)
+
+let uses_parser : string key_parser = fun orig args ->
+ assert_once ~name:"using" orig;
+ match args with
+ | VernacFlagLeaf str -> str
+ | _ -> CErrors.user_err (Pp.str "Ill formed \"using\" attribute")
+
+let using = attribute_of_list ["using",uses_parser]
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 51bab79938..1969665082 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -51,6 +51,7 @@ val option_locality : Goptions.option_locality attribute
val deprecation : Deprecation.t option attribute
val canonical_field : bool attribute
val canonical_instance : bool attribute
+val using : string option attribute
val program_mode_option_name : string list
(** For internal use when messing with the global option. *)
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 7a7e7d6e35..f715459616 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -145,7 +145,7 @@ let build_beq_scheme_deps kn =
| Cast (x,_,_) -> aux accu (Term.applist (x,a))
| App _ -> assert false
| Ind ((kn', _), _) ->
- if MutInd.equal kn kn' then accu
+ if Environ.QMutInd.equal env kn kn' then accu
else
let eff = SchemeMutualDep (kn', !beq_scheme_kind_aux ()) in
List.fold_left aux (eff :: accu) a
@@ -253,7 +253,7 @@ let build_beq_scheme mode kn =
| Cast (x,_,_) -> aux (Term.applist (x,a))
| App _ -> assert false
| Ind ((kn',i as ind'),u) (*FIXME: universes *) ->
- if MutInd.equal kn kn' then mkRel(eqA-nlist-i+nb_ind-1)
+ if Environ.QMutInd.equal env kn kn' then mkRel(eqA-nlist-i+nb_ind-1)
else begin
try
let eq = match lookup_scheme (!beq_scheme_kind_aux()) ind' with
@@ -496,7 +496,7 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
let u,v = try destruct_ind env sigma tt1
(* trick so that the good sequence is returned*)
with e when CErrors.noncritical e -> indu,[||]
- in if eq_ind (fst u) ind
+ in if Ind.CanOrd.equal (fst u) ind
then Tacticals.New.tclTHENLIST [Equality.replace t1 t2; Auto.default_auto ; aux q1 q2 ]
else (
find_scheme bl_scheme_key (fst u) (*FIXME*) >>= fun c ->
@@ -539,7 +539,8 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.")
end
end >>= fun (sp2,i2) ->
- if not (MutInd.equal sp1 sp2) || not (Int.equal i1 i2)
+ Proofview.tclENV >>= fun env ->
+ if not (Environ.QMutInd.equal env sp1 sp2) || not (Int.equal i1 i2)
then Tacticals.New.tclZEROMSG (str "Eq should be on the same type")
else aux (Array.to_list ca1) (Array.to_list ca2)
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index c1dbf0a1ea..3fc74cba5b 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -110,7 +110,7 @@ let interp_definition ~program_mode env evd impl_env bl red_option c ctypopt =
let tyopt = Option.map (fun ty -> EConstr.it_mkProd_or_LetIn ty ctx) tyopt in
evd, (c, tyopt), imps
-let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
+let do_definition ?hook ~name ~scope ~poly ~kind ?using udecl bl red_option c ctypopt =
let program_mode = false in
let env = Global.env() in
(* Explicitly bound universes and constraints *)
@@ -118,14 +118,19 @@ let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
let evd, (body, types), impargs =
interp_definition ~program_mode env evd empty_internalization_env bl red_option c ctypopt
in
+ let using = using |> Option.map (fun expr ->
+ let terms = body :: match types with Some x -> [x] | None -> [] in
+ let l = Proof_using.process_expr (Global.env()) evd expr terms in
+ Names.Id.Set.(List.fold_right add l empty))
+ in
let kind = Decls.IsDefinition kind in
- let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types () in
+ let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types ?using () in
let info = Declare.Info.make ~scope ~kind ?hook ~udecl ~poly () in
let _ : Names.GlobRef.t =
Declare.declare_definition ~info ~cinfo ~opaque:false ~body evd
in ()
-let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
+let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind ?using udecl bl red_option c ctypopt =
let program_mode = true in
let env = Global.env() in
(* Explicitly bound universes and constraints *)
@@ -133,9 +138,14 @@ let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind udecl bl red_option
let evd, (body, types), impargs =
interp_definition ~program_mode env evd empty_internalization_env bl red_option c ctypopt
in
+ let using = using |> Option.map (fun expr ->
+ let terms = body :: match types with Some x -> [x] | None -> [] in
+ let l = Proof_using.process_expr (Global.env()) evd expr terms in
+ Names.Id.Set.(List.fold_right add l empty))
+ in
let term, typ, uctx, obls = Declare.Obls.prepare_obligation ~name ~body ~types evd in
let pm, _ =
- let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in
+ let cinfo = Declare.CInfo.make ~name ~typ ~impargs ?using () in
let info = Declare.Info.make ~udecl ~scope ~poly ~kind ?hook () in
Declare.Obls.add_definition ~pm ~cinfo ~info ~term ~uctx obls
in pm
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 7420235449..5e1b705ae4 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -31,6 +31,7 @@ val do_definition
-> scope:Locality.locality
-> poly:bool
-> kind:Decls.definition_object_kind
+ -> ?using:Vernacexpr.section_subset_expr
-> universe_decl_expr option
-> local_binder_expr list
-> red_expr option
@@ -45,6 +46,7 @@ val do_definition_program
-> scope:Locality.locality
-> poly:bool
-> kind:Decls.logical_kind
+ -> ?using:Vernacexpr.section_subset_expr
-> universe_decl_expr option
-> local_binder_expr list
-> red_expr option
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 78572c6aa6..29bf5fbcc2 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -251,15 +251,22 @@ let interp_fixpoint ?(check_recursivity=true) ~cofix l :
let uctx,fix = ground_fixpoint env evd fix in
(fix,pl,uctx,info)
-let build_recthms ~indexes fixnames fixtypes fiximps =
+let build_recthms ~indexes ?using fixnames fixtypes fiximps =
let fix_kind, cofix = match indexes with
| Some indexes -> Decls.Fixpoint, false
| None -> Decls.CoFixpoint, true
in
let thms =
List.map3 (fun name typ (ctx,impargs,_) ->
+ let using = using |> Option.map (fun expr ->
+ let terms = [EConstr.of_constr typ] in
+ let env = Global.env() in
+ let sigma = Evd.from_env env in
+ let l = Proof_using.process_expr env sigma expr terms in
+ Names.Id.Set.(List.fold_right add l empty))
+ in
let args = List.map Context.Rel.Declaration.get_name ctx in
- Declare.CInfo.make ~name ~typ ~args ~impargs ()
+ Declare.CInfo.make ~name ~typ ~args ~impargs ?using ()
) fixnames fixtypes fiximps
in
fix_kind, cofix, thms
@@ -277,9 +284,9 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs
List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
lemma
-let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns =
+let declare_fixpoint_generic ?indexes ~scope ~poly ?using ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns =
(* We shortcut the proof process *)
- let fix_kind, cofix, fixitems = build_recthms ~indexes fixnames fixtypes fiximps in
+ let fix_kind, cofix, fixitems = build_recthms ~indexes ?using fixnames fixtypes fiximps in
let fixdefs = List.map Option.get fixdefs in
let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
let fix_kind = Decls.IsDefinition fix_kind in
@@ -328,9 +335,9 @@ let do_fixpoint_interactive ~scope ~poly l : Declare.Proof.t =
let lemma = declare_fixpoint_interactive_generic ~indexes:possible_indexes ~scope ~poly fix ntns in
lemma
-let do_fixpoint ~scope ~poly l =
+let do_fixpoint ~scope ~poly ?using l =
let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in
- declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly fix ntns
+ declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly ?using fix ntns
let do_cofixpoint_common (fixl : Vernacexpr.cofixpoint_expr list) =
let fixl = List.map (fun fix -> {fix with Vernacexpr.rec_order = None}) fixl in
@@ -342,6 +349,6 @@ let do_cofixpoint_interactive ~scope ~poly l =
let lemma = declare_fixpoint_interactive_generic ~scope ~poly cofix ntns in
lemma
-let do_cofixpoint ~scope ~poly l =
+let do_cofixpoint ~scope ~poly ?using l =
let cofix, ntns = do_cofixpoint_common l in
- declare_fixpoint_generic ~scope ~poly cofix ntns
+ declare_fixpoint_generic ~scope ~poly ?using cofix ntns
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index aa5446205c..a36aba7672 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -19,13 +19,13 @@ val do_fixpoint_interactive :
scope:Locality.locality -> poly:bool -> fixpoint_expr list -> Declare.Proof.t
val do_fixpoint :
- scope:Locality.locality -> poly:bool -> fixpoint_expr list -> unit
+ scope:Locality.locality -> poly:bool -> ?using:Vernacexpr.section_subset_expr -> fixpoint_expr list -> unit
val do_cofixpoint_interactive :
scope:Locality.locality -> poly:bool -> cofixpoint_expr list -> Declare.Proof.t
val do_cofixpoint :
- scope:Locality.locality -> poly:bool -> cofixpoint_expr list -> unit
+ scope:Locality.locality -> poly:bool -> ?using:Vernacexpr.section_subset_expr -> cofixpoint_expr list -> unit
(************************************************************************)
(** Internal API *)
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 55901fd604..9623317ddf 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -109,7 +109,7 @@ let telescope env sigma l =
let nf_evar_context sigma ctx =
List.map (map_constr (fun c -> Evarutil.nf_evar sigma c)) ctx
-let build_wellfounded pm (recname,pl,bl,arityc,body) poly r measure notation =
+let build_wellfounded pm (recname,pl,bl,arityc,body) poly ?using r measure notation =
let open EConstr in
let open Vars in
let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in
@@ -259,8 +259,13 @@ let build_wellfounded pm (recname,pl,bl,arityc,body) poly r measure notation =
let evars, _, evars_def, evars_typ =
RetrieveObl.retrieve_obligations env recname sigma 0 def typ
in
+ let using = using |> Option.map (fun expr ->
+ let terms = List.map EConstr.of_constr [evars_def; evars_typ] in
+ let l = Proof_using.process_expr env sigma expr terms in
+ Names.Id.Set.(List.fold_right add l empty))
+ in
let uctx = Evd.evar_universe_context sigma in
- let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ () in
+ let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ ?using () in
let info = Declare.Info.make ~udecl ~poly ~hook () in
let pm, _ =
Declare.Obls.add_definition ~pm ~cinfo ~info ~term:evars_def ~uctx evars in
@@ -275,7 +280,7 @@ let collect_evars_of_term evd c ty =
Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
evars (Evd.from_ctx (Evd.evar_universe_context evd))
-let do_program_recursive ~pm ~scope ~poly fixkind fixl =
+let do_program_recursive ~pm ~scope ~poly ?using fixkind fixl =
let cofix = fixkind = Declare.Obls.IsCoFixpoint in
let (env, rec_sign, udecl, evd), fix, info =
interp_recursive ~cofix ~program_mode:true fixl
@@ -287,13 +292,18 @@ let do_program_recursive ~pm ~scope ~poly fixkind fixl =
let evd = nf_evar_map_undefined evd in
let collect_evars name def typ impargs =
(* Generalize by the recursive prototypes *)
+ let using = using |> Option.map (fun expr ->
+ let terms = [def; typ] in
+ let l = Proof_using.process_expr env evd expr terms in
+ Names.Id.Set.(List.fold_right add l empty))
+ in
let def = nf_evar evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) in
let typ = nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in
let evm = collect_evars_of_term evd def typ in
let evars, _, def, typ =
RetrieveObl.retrieve_obligations env name evm
(List.length rec_sign) def typ in
- let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in
+ let cinfo = Declare.CInfo.make ~name ~typ ~impargs ?using () in
(cinfo, def, evars)
in
let (fixnames,fixrs,fixdefs,fixtypes) = fix in
@@ -325,13 +335,13 @@ let do_program_recursive ~pm ~scope ~poly fixkind fixl =
let info = Declare.Info.make ~poly ~scope ~kind ~udecl () in
Declare.Obls.add_mutual_definitions ~pm defs ~info ~uctx ~ntns fixkind
-let do_fixpoint ~pm ~scope ~poly l =
+let do_fixpoint ~pm ~scope ~poly ?using l =
let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in
match g, l with
| [Some { CAst.v = CWfRec (n,r) }],
[ Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations} ] ->
let recarg = mkIdentC n.CAst.v in
- build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly r recarg notations
+ build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly ?using r recarg notations
| [Some { CAst.v = CMeasureRec (n, m, r) }],
[Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations }] ->
@@ -344,7 +354,7 @@ let do_fixpoint ~pm ~scope ~poly l =
user_err Pp.(str"Measure takes only two arguments in Program Fixpoint.")
| _, _ -> r
in
- build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly
+ build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly ?using
(Option.default (CAst.make @@ CRef (lt_ref,None)) r) m notations
| _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g ->
@@ -352,11 +362,11 @@ let do_fixpoint ~pm ~scope ~poly l =
Vernacexpr.(ComFixpoint.adjust_rec_order ~structonly:true fix.binders fix.rec_order)) l in
let fixkind = Declare.Obls.IsFixpoint annots in
let l = List.map2 (fun fix rec_order -> { fix with Vernacexpr.rec_order }) l annots in
- do_program_recursive ~pm ~scope ~poly fixkind l
+ do_program_recursive ~pm ~scope ~poly ?using fixkind l
| _, _ ->
CErrors.user_err ~hdr:"do_fixpoint"
(str "Well-founded fixpoints not allowed in mutually recursive blocks")
-let do_cofixpoint ~pm ~scope ~poly fixl =
+let do_cofixpoint ~pm ~scope ~poly ?using fixl =
let fixl = List.map (fun fix -> { fix with Vernacexpr.rec_order = None }) fixl in
- do_program_recursive ~pm ~scope ~poly Declare.Obls.IsCoFixpoint fixl
+ do_program_recursive ~pm ~scope ~poly ?using Declare.Obls.IsCoFixpoint fixl
diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli
index 7935cf27fb..30bf3ae8f8 100644
--- a/vernac/comProgramFixpoint.mli
+++ b/vernac/comProgramFixpoint.mli
@@ -15,6 +15,7 @@ val do_fixpoint :
pm:Declare.OblState.t
-> scope:Locality.locality
-> poly:bool
+ -> ?using:Vernacexpr.section_subset_expr
-> fixpoint_expr list
-> Declare.OblState.t
@@ -22,5 +23,6 @@ val do_cofixpoint :
pm:Declare.OblState.t
-> scope:Locality.locality
-> poly:bool
+ -> ?using:Vernacexpr.section_subset_expr
-> cofixpoint_expr list
-> Declare.OblState.t
diff --git a/vernac/comTactic.ml b/vernac/comTactic.ml
index 8a9a412362..2252d46e58 100644
--- a/vernac/comTactic.ml
+++ b/vernac/comTactic.ml
@@ -16,13 +16,13 @@ module DMap = Dyn.Map(struct type 'a t = 'a -> unit Proofview.tactic end)
let interp_map = ref DMap.empty
-type 'a tactic_interpreter = 'a Dyn.tag
-type interpretable = I : 'a tactic_interpreter * 'a -> interpretable
+type interpretable = I : 'a Dyn.tag * 'a -> interpretable
+type 'a tactic_interpreter = Interpreter of ('a -> interpretable)
let register_tactic_interpreter na f =
let t = Dyn.create na in
interp_map := DMap.add t f !interp_map;
- t
+ Interpreter (fun x -> I (t,x))
let interp_tac (I (tag,t)) =
let f = DMap.find tag !interp_map in
diff --git a/vernac/comTactic.mli b/vernac/comTactic.mli
index f1a75e1b6a..72e71d013a 100644
--- a/vernac/comTactic.mli
+++ b/vernac/comTactic.mli
@@ -9,10 +9,13 @@
(************************************************************************)
(** Tactic interpreters have to register their interpretation function *)
-type 'a tactic_interpreter
-type interpretable = I : 'a tactic_interpreter * 'a -> interpretable
+type interpretable
-(** ['a] should be marshallable if ever used with [par:] *)
+type 'a tactic_interpreter = private Interpreter of ('a -> interpretable)
+
+(** ['a] should be marshallable if ever used with [par:]. Must be
+ called no more than once per process with a particular string: make
+ sure to use partial application. *)
val register_tactic_interpreter :
string -> ('a -> unit Proofview.tactic) -> 'a tactic_interpreter
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 5274a6da3b..0baae6eca5 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -55,11 +55,13 @@ module CInfo = struct
(** Names to pre-introduce *)
; impargs : Impargs.manual_implicits
(** Explicitily declared implicit arguments *)
+ ; using : Names.Id.Set.t option
+ (** Explicit declaration of section variables used by the constant *)
}
- let make ~name ~typ ?(args=[]) ?(impargs=[]) () =
- { name; typ; args; impargs }
+ let make ~name ~typ ?(args=[]) ?(impargs=[]) ?using () =
+ { name; typ; args; impargs; using }
let to_constr sigma thm = { thm with typ = EConstr.to_constr sigma thm.typ }
@@ -108,10 +110,10 @@ let default_univ_entry = Entries.Monomorphic_entry Univ.ContextSet.empty
(** [univsbody] are universe-constraints attached to the body-only,
used in vio-delayed opaque constants and private poly universes *)
-let definition_entry_core ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types
+let definition_entry_core ?(opaque=false) ?using ?(inline=false) ?feedback_id ?types
?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) ?(univsbody=Univ.ContextSet.empty) body =
{ proof_entry_body = Future.from_val ((body,univsbody), eff);
- proof_entry_secctx = section_vars;
+ proof_entry_secctx = using;
proof_entry_type = types;
proof_entry_universes = univs;
proof_entry_opaque = opaque;
@@ -119,7 +121,7 @@ let definition_entry_core ?(opaque=false) ?(inline=false) ?feedback_id ?section_
proof_entry_inline_code = inline}
let definition_entry =
- definition_entry_core ?eff:None ?univsbody:None ?feedback_id:None ?section_vars:None
+ definition_entry_core ?eff:None ?univsbody:None ?feedback_id:None
type 'a constant_entry =
| DefinitionEntry of 'a proof_entry
@@ -162,7 +164,7 @@ let cache_constant ((sp,kn), obj) =
then Constant.make1 kn
else CErrors.anomaly Pp.(str"Missing constant " ++ Id.print(Libnames.basename sp) ++ str".")
in
- assert (Constant.equal kn' (Constant.make1 kn));
+ assert (Environ.QConstant.equal (Global.env ()) kn' (Constant.make1 kn));
Nametab.push (Nametab.Until 1) sp (GlobRef.ConstRef (Constant.make1 kn));
Dumpglob.add_constant_kind (Constant.make1 kn) obj.cst_kind
@@ -236,9 +238,9 @@ let pure_definition_entry ?(opaque=false) ?(inline=false) ?types
proof_entry_feedback = None;
proof_entry_inline_code = inline}
-let delayed_definition_entry ~opaque ?feedback_id ~section_vars ~univs ?types body =
+let delayed_definition_entry ~opaque ?feedback_id ~using ~univs ?types body =
{ proof_entry_body = body
- ; proof_entry_secctx = section_vars
+ ; proof_entry_secctx = using
; proof_entry_type = types
; proof_entry_universes = univs
; proof_entry_opaque = opaque
@@ -608,8 +610,8 @@ let declare_mutually_recursive_core ~info ~cinfo ~opaque ~ntns ~uctx ~rec_declar
uctx, univs
in
let csts = CList.map2
- (fun CInfo.{ name; typ; impargs } body ->
- let entry = definition_entry ~opaque ~types:typ ~univs body in
+ (fun CInfo.{ name; typ; impargs; using } body ->
+ let entry = definition_entry ~opaque ~types:typ ~univs ?using body in
declare_entry ~name ~scope ~kind ~impargs ~uctx entry)
cinfo fixdecls
in
@@ -660,7 +662,7 @@ let check_evars_are_solved env sigma t =
let evars = Evarutil.undefined_evars_of_term sigma t in
if not (Evar.Set.is_empty evars) then error_unresolved_evars env sigma t evars
-let prepare_definition ~info ~opaque ~body ~typ sigma =
+let prepare_definition ~info ~opaque ?using ~body ~typ sigma =
let { Info.poly; udecl; inline; _ } = info in
let env = Global.env () in
let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false
@@ -669,13 +671,13 @@ let prepare_definition ~info ~opaque ~body ~typ sigma =
Option.iter (check_evars_are_solved env sigma) types;
check_evars_are_solved env sigma body;
let univs = Evd.check_univ_decl ~poly sigma udecl in
- let entry = definition_entry ~opaque ~inline ?types ~univs body in
+ let entry = definition_entry ~opaque ?using ~inline ?types ~univs body in
let uctx = Evd.evar_universe_context sigma in
entry, uctx
let declare_definition_core ~info ~cinfo ~opaque ~obls ~body sigma =
- let { CInfo.name; impargs; typ; _ } = cinfo in
- let entry, uctx = prepare_definition ~info ~opaque ~body ~typ sigma in
+ let { CInfo.name; impargs; typ; using; _ } = cinfo in
+ let entry, uctx = prepare_definition ~info ~opaque ?using ~body ~typ sigma in
let { Info.scope; kind; hook; _ } = info in
declare_entry_core ~name ~scope ~kind ~impargs ~obls ?hook ~uctx entry, uctx
@@ -803,6 +805,7 @@ module ProgramDecl = struct
let set_uctx ~uctx prg = {prg with prg_uctx = uctx}
let get_poly prg = prg.prg_info.Info.poly
let get_obligations prg = prg.prg_obligations
+ let get_using prg = prg.prg_cinfo.CInfo.using
end
end
@@ -1137,7 +1140,7 @@ let declare_mutual_definition ~pm l =
in
let term = EConstr.to_constr sigma term in
let typ = EConstr.to_constr sigma typ in
- let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_cinfo.CInfo.impargs) in
+ let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_cinfo.CInfo.impargs, x.prg_cinfo.CInfo.using) in
let oblsubst = List.map (fun (id, (_, c)) -> (id, c)) oblsubst in
(def, oblsubst)
in
@@ -1151,11 +1154,11 @@ let declare_mutual_definition ~pm l =
(* let fixdefs = List.map reduce_fix fixdefs in *)
let fixdefs, fixrs, fixtypes, fixitems =
List.fold_right2
- (fun (d, r, typ, impargs) name (a1, a2, a3, a4) ->
+ (fun (d, r, typ, impargs, using) name (a1, a2, a3, a4) ->
( d :: a1
, r :: a2
, typ :: a3
- , CInfo.{name; typ; impargs; args = []} :: a4 ))
+ , CInfo.{name; typ; impargs; args = []; using } :: a4 ))
defs first.prg_deps ([], [], [], [])
in
let fixkind = Option.get first.prg_fixkind in
@@ -1376,7 +1379,7 @@ end
type t =
{ endline_tactic : Genarg.glob_generic_argument option
- ; section_vars : Id.Set.t option
+ ; using : Id.Set.t option
; proof : Proof.t
; initial_euctx : UState.t
(** The initial universe context (for the statement) *)
@@ -1435,7 +1438,7 @@ let start_proof_core ~name ~typ ~pinfo ?(sign=initialize_named_context_for_proof
let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
{ proof
; endline_tactic = None
- ; section_vars = None
+ ; using = None
; initial_euctx
; pinfo
}
@@ -1458,7 +1461,7 @@ let start_dependent ~info ~name ~proof_ending goals =
let pinfo = Proof_info.make ~info ~cinfo ~proof_ending () in
{ proof
; endline_tactic = None
- ; section_vars = None
+ ; using = None
; initial_euctx
; pinfo
}
@@ -1523,7 +1526,7 @@ let start_mutual_with_initialization ~info ~cinfo ~mutual_info sigma snl =
map lemma ~f:(fun p ->
pi1 @@ Proof.run_tactic Global.(env ()) init_tac p)
-let get_used_variables pf = pf.section_vars
+let get_used_variables pf = pf.using
let get_universe_decl pf = pf.pinfo.Proof_info.info.Info.udecl
let set_used_variables ps l =
@@ -1547,9 +1550,9 @@ let set_used_variables ps l =
else (ctx, all_safe) in
let ctx, _ =
Environ.fold_named_context aux env ~init:(ctx,ctx_set) in
- if not (Option.is_empty ps.section_vars) then
+ if not (Option.is_empty ps.using) then
CErrors.user_err Pp.(str "Used section variables can be declared only once");
- ctx, { ps with section_vars = Some (Context.Named.to_vars ctx) }
+ ctx, { ps with using = Some (Context.Named.to_vars ctx) }
let get_open_goals ps =
let Proof.{ goals; stack; sigma } = Proof.data ps.proof in
@@ -1646,7 +1649,7 @@ let make_univs ~poly ~uctx ~udecl (used_univs_typ, typ) (used_univs_body, body)
let close_proof ~opaque ~keep_body_ucst_separate ps =
- let { section_vars; proof; initial_euctx; pinfo } = ps in
+ let { using; proof; initial_euctx; pinfo } = ps in
let { Proof_info.info = { Info.udecl } } = pinfo in
let { Proof.name; poly } = Proof.data proof in
let unsafe_typ = keep_body_ucst_separate && not poly in
@@ -1667,7 +1670,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ps =
then make_univs_private_poly ~poly ~uctx ~udecl t b
else make_univs ~poly ~uctx ~udecl t b
in
- definition_entry_core ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body
+ definition_entry_core ~opaque ?using ~univs:utyp ~univsbody:ubody ~types:typ ~eff body
in
let entries = CList.map make_entry elist in
{ name; entries; uctx }
@@ -1675,7 +1678,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ps =
type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t
let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.computation) =
- let { section_vars; proof; initial_euctx; pinfo } = ps in
+ let { using; proof; initial_euctx; pinfo } = ps in
let { Proof_info.info = { Info.udecl } } = pinfo in
let { Proof.name; poly; entry; sigma } = Proof.data proof in
@@ -1712,7 +1715,7 @@ let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.comput
let univs = UState.restrict uctx used_univs in
let univs = UState.check_mono_univ_decl univs udecl in
(pt,univs),eff)
- |> delayed_definition_entry ~opaque ~feedback_id ~section_vars ~univs ~types
+ |> delayed_definition_entry ~opaque ~feedback_id ~using ~univs ~types
in
let entries = Future.map2 make_entry fpl (Proofview.initial_goals entry) in
{ name; entries; uctx = initial_euctx }
@@ -2206,26 +2209,60 @@ let warn_solve_errored =
; fnl ()
; str "This will become an error in the future" ])
-let solve_by_tac ?loc name evi t ~poly ~uctx =
- (* the status is dropped. *)
+let solve_by_tac prg obls i tac =
+ let obl = obls.(i) in
+ let obl = subst_deps_obl obls obl in
+ let tac = Option.(default !default_tactic (append tac obl.obl_tac)) in
+ let uctx = Internal.get_uctx prg in
+ let uctx = UState.update_sigma_univs uctx (Global.universes ()) in
+ let poly = Internal.get_poly prg in
+ let evi = evar_of_obligation obl in
+ (* the status of [build_by_tactic] is dropped. *)
try
let env = Global.env () in
let body, types, _univs, _, uctx =
- build_by_tactic env ~uctx ~poly ~typ:evi.evar_concl t in
+ build_by_tactic env ~uctx ~poly ~typ:evi.evar_concl tac in
Inductiveops.control_only_guard env (Evd.from_ctx uctx) (EConstr.of_constr body);
Some (body, types, uctx)
with
| Tacticals.FailError (_, s) as exn ->
let _ = Exninfo.capture exn in
+ let loc = fst obl.obl_location in
CErrors.user_err ?loc ~hdr:"solve_obligation" (Lazy.force s)
(* If the proof is open we absorb the error and leave the obligation open *)
| Proof_.OpenProof _ ->
None
| e when CErrors.noncritical e ->
let err = CErrors.print e in
+ let loc = fst obl.obl_location in
warn_solve_errored ?loc err;
None
+let solve_and_declare_by_tac prg obls i tac =
+ match solve_by_tac prg obls i tac with
+ | None -> None
+ | Some (t, ty, uctx) ->
+ let obl = obls.(i) in
+ let poly = Internal.get_poly prg in
+ let prg = ProgramDecl.Internal.set_uctx ~uctx prg in
+ let def, obl', _cst = declare_obligation prg obl ~body:t ~types:ty ~uctx in
+ obls.(i) <- obl';
+ if def && not poly then (
+ (* Declare the term constraints with the first obligation only *)
+ let uctx_global = UState.from_env (Global.env ()) in
+ let uctx = UState.merge_subst uctx_global (UState.subst uctx) in
+ Some (ProgramDecl.Internal.set_uctx ~uctx prg))
+ else Some prg
+
+let solve_obligation_by_tac prg obls i tac =
+ let obl = obls.(i) in
+ match obl.obl_body with
+ | Some _ -> None
+ | None ->
+ if List.is_empty (deps_remaining obls obl.obl_deps)
+ then solve_and_declare_by_tac prg obls i tac
+ else None
+
let get_unique_prog ~pm prg =
match State.get_unique_open_prog pm prg with
| Ok prg -> prg
@@ -2255,7 +2292,8 @@ let rec solve_obligation prg num tac =
let name = Internal.get_name prg in
Proof_ending.End_obligation {name; num; auto}
in
- let cinfo = CInfo.make ~name:obl.obl_name ~typ:(EConstr.of_constr obl.obl_type) () in
+ let using = Internal.get_using prg in
+ let cinfo = CInfo.make ~name:obl.obl_name ~typ:(EConstr.of_constr obl.obl_type) ?using () in
let poly = Internal.get_poly prg in
let info = Info.make ~scope ~kind ~poly () in
let lemma = Proof.start_core ~cinfo ~info ~proof_ending evd in
@@ -2263,49 +2301,6 @@ let rec solve_obligation prg num tac =
let lemma = Option.cata (fun tac -> Proof.set_endline_tactic tac lemma) lemma tac in
lemma
-and obligation (user_num, name, typ) ~pm tac =
- let num = pred user_num in
- let prg = get_unique_prog ~pm name in
- let { obls; remaining } = Internal.get_obligations prg in
- if num >= 0 && num < Array.length obls then
- let obl = obls.(num) in
- match obl.obl_body with
- | None -> solve_obligation prg num tac
- | Some r -> Error.already_solved num
- else Error.unknown_obligation num
-
-and solve_obligation_by_tac prg obls i tac =
- let obl = obls.(i) in
- match obl.obl_body with
- | Some _ -> None
- | None ->
- if List.is_empty (deps_remaining obls obl.obl_deps) then
- let obl = subst_deps_obl obls obl in
- let tac =
- match tac with
- | Some t -> t
- | None ->
- match obl.obl_tac with
- | Some t -> t
- | None -> !default_tactic
- in
- let uctx = Internal.get_uctx prg in
- let uctx = UState.update_sigma_univs uctx (Global.universes ()) in
- let poly = Internal.get_poly prg in
- match solve_by_tac ?loc:(fst obl.obl_location) obl.obl_name (evar_of_obligation obl) tac ~poly ~uctx with
- | None -> None
- | Some (t, ty, uctx) ->
- let prg = ProgramDecl.Internal.set_uctx ~uctx prg in
- let def, obl', _cst = declare_obligation prg obl ~body:t ~types:ty ~uctx in
- obls.(i) <- obl';
- if def && not poly then (
- (* Declare the term constraints with the first obligation only *)
- let uctx_global = UState.from_env (Global.env ()) in
- let uctx = UState.merge_subst uctx_global (UState.subst uctx) in
- Some (ProgramDecl.Internal.set_uctx ~uctx prg))
- else Some prg
- else None
-
and solve_prg_obligations ~pm prg ?oblset tac =
let { obls; remaining } = Internal.get_obligations prg in
let rem = ref remaining in
@@ -2332,15 +2327,21 @@ and solve_prg_obligations ~pm prg ?oblset tac =
in
update_obls ~pm prg obls' !rem
-and solve_obligations ~pm n tac =
+and auto_solve_obligations ~pm n ?oblset tac : State.t * progress =
+ Flags.if_verbose Feedback.msg_info
+ (str "Solving obligations automatically...");
+ let prg = get_unique_prog ~pm n in
+ solve_prg_obligations ~pm prg ?oblset tac
+
+let solve_obligations ~pm n tac =
let prg = get_unique_prog ~pm n in
solve_prg_obligations ~pm prg tac
-and solve_all_obligations ~pm tac =
+let solve_all_obligations ~pm tac =
State.fold pm ~init:pm ~f:(fun k v pm ->
solve_prg_obligations ~pm v tac |> fst)
-and try_solve_obligation ~pm n prg tac =
+let try_solve_obligation ~pm n prg tac =
let prg = get_unique_prog ~pm prg in
let {obls; remaining} = Internal.get_obligations prg in
let obls' = Array.copy obls in
@@ -2350,14 +2351,19 @@ and try_solve_obligation ~pm n prg tac =
pm
| None -> pm
-and try_solve_obligations ~pm n tac =
+let try_solve_obligations ~pm n tac =
solve_obligations ~pm n tac |> fst
-and auto_solve_obligations ~pm n ?oblset tac : State.t * progress =
- Flags.if_verbose Feedback.msg_info
- (str "Solving obligations automatically...");
- let prg = get_unique_prog ~pm n in
- solve_prg_obligations ~pm prg ?oblset tac
+let obligation (user_num, name, typ) ~pm tac =
+ let num = pred user_num in
+ let prg = get_unique_prog ~pm name in
+ let { obls; remaining } = Internal.get_obligations prg in
+ if num >= 0 && num < Array.length obls then
+ let obl = obls.(num) in
+ match obl.obl_body with
+ | None -> solve_obligation prg num tac
+ | Some r -> Error.already_solved num
+ else Error.unknown_obligation num
let show_single_obligation i n obls x =
let x = subst_deps_obl obls x in
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 1ad79928d5..0520bf8717 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -79,6 +79,7 @@ module CInfo : sig
-> typ:'constr
-> ?args:Name.t list
-> ?impargs:Impargs.manual_implicits
+ -> ?using:Names.Id.Set.t
-> unit
-> 'constr t
@@ -244,6 +245,12 @@ module Proof : sig
* (w.r.t. type dependencies and let-ins covered by it) *)
val set_used_variables : t -> Names.Id.t list -> Constr.named_context * t
+ (** Gets the set of variables declared to be used by the proof. None means
+ no "Proof using" or #[using] was given *)
+ val get_used_variables : t -> Id.Set.t option
+
+ (** Compacts the representation of the proof by pruning all intermediate
+ terms *)
val compact : t -> t
(** Update the proof's universe information typically after a
@@ -333,6 +340,7 @@ type 'a proof_entry
val definition_entry
: ?opaque:bool
+ -> ?using:Names.Id.Set.t
-> ?inline:bool
-> ?types:Constr.types
-> ?univs:Entries.universes_entry
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index b134f7b82b..123ea2c24e 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -300,13 +300,13 @@ let interp_constr_entry_key : type r. _ -> r target -> int -> r Entry.t * int op
match forpat with
| ForConstr ->
if level = 200 then Constr.binder_constr, None
- else Constr.operconstr, Some level
+ else Constr.term, Some level
| ForPattern -> Constr.pattern, Some level
let target_entry : type s. notation_entry -> s target -> s Entry.t = function
| InConstrEntry ->
(function
- | ForConstr -> Constr.operconstr
+ | ForConstr -> Constr.term
| ForPattern -> Constr.pattern)
| InCustomEntry s ->
let (entry_for_constr, entry_for_patttern) = find_custom_entry s in
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index dfc7b05b51..f192d67624 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -48,7 +48,7 @@ let assumption_token = Entry.create "assumption_token"
let def_body = Entry.create "def_body"
let decl_notations = Entry.create "decl_notations"
let record_field = Entry.create "record_field"
-let of_type_with_opt_coercion = Entry.create "of_type_with_opt_coercion"
+let of_type = Entry.create "of_type"
let section_subset_expr = Entry.create "section_subset_expr"
let scope_delimiter = Entry.create "scope_delimiter"
let syntax_modifiers = Entry.create "syntax_modifiers"
@@ -113,10 +113,11 @@ GRAMMAR EXTEND Gram
]
;
attribute:
- [ [ k = ident ; v = attribute_value -> { Names.Id.to_string k, v } ]
+ [ [ k = ident ; v = attr_value -> { Names.Id.to_string k, v }
+ | "using" ; v = attr_value -> { "using", v } ]
]
;
- attribute_value:
+ attr_value:
[ [ "=" ; v = string -> { VernacFlagLeaf v }
| "(" ; a = attribute_list ; ")" -> { VernacFlagList a }
| -> { VernacFlagEmpty } ]
@@ -196,8 +197,8 @@ let name_of_ident_decl : ident_decl -> name_decl =
(* Gallina declarations *)
GRAMMAR EXTEND Gram
- GLOBAL: gallina gallina_ext thm_token def_token assumption_token def_body of_type_with_opt_coercion
- record_field decl_notations rec_definition ident_decl univ_decl;
+ GLOBAL: gallina gallina_ext thm_token def_token assumption_token def_body of_type
+ record_field decl_notations fix_definition ident_decl univ_decl;
gallina:
(* Definition, Theorem, Variable, Axiom, ... *)
@@ -219,13 +220,13 @@ GRAMMAR EXTEND Gram
(* Gallina inductive declarations *)
| f = finite_token; indl = LIST1 inductive_definition SEP "with" ->
{ VernacInductive (f, indl) }
- | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
+ | "Fixpoint"; recs = LIST1 fix_definition SEP "with" ->
{ VernacFixpoint (NoDischarge, recs) }
- | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
+ | IDENT "Let"; "Fixpoint"; recs = LIST1 fix_definition SEP "with" ->
{ VernacFixpoint (DoDischarge, recs) }
- | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
+ | "CoFixpoint"; corecs = LIST1 cofix_definition SEP "with" ->
{ VernacCoFixpoint (NoDischarge, corecs) }
- | IDENT "Let"; "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
+ | IDENT "Let"; "CoFixpoint"; corecs = LIST1 cofix_definition SEP "with" ->
{ VernacCoFixpoint (DoDischarge, corecs) }
| IDENT "Scheme"; l = LIST1 scheme SEP "with" -> { VernacScheme l }
| IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from";
@@ -339,7 +340,7 @@ GRAMMAR EXTEND Gram
;
(* Inductives and records *)
opt_constructors_or_fields:
- [ [ ":="; lc = constructor_list_or_record_decl -> { lc }
+ [ [ ":="; lc = constructors_or_record -> { lc }
| -> { RecordDecl (None, []) } ] ]
;
inductive_definition:
@@ -349,7 +350,7 @@ GRAMMAR EXTEND Gram
lc=opt_constructors_or_fields; ntn = decl_notations ->
{ (((oc,id),(indpar,extrapar),c,lc),ntn) } ] ]
;
- constructor_list_or_record_decl:
+ constructors_or_record:
[ [ "|"; l = LIST1 constructor SEP "|" -> { Constructors l }
| id = identref ; c = constructor_type; "|"; l = LIST1 constructor SEP "|" ->
{ Constructors ((c id)::l) }
@@ -369,7 +370,7 @@ GRAMMAR EXTEND Gram
| -> { false } ] ]
;
(* (co)-fixpoints *)
- rec_definition:
+ fix_definition:
[ [ id_decl = ident_decl;
bl = binders_fixannot;
rtype = type_cstr;
@@ -378,7 +379,7 @@ GRAMMAR EXTEND Gram
{fname = fst id_decl; univs = snd id_decl; rec_order; binders; rtype; body_def; notations}
} ] ]
;
- corec_definition:
+ cofix_definition:
[ [ id_decl = ident_decl; binders = binders; rtype = type_cstr;
body_def = OPT [":="; def = lconstr -> { def }]; notations = decl_notations ->
{ {fname = fst id_decl; univs = snd id_decl; rec_order = (); binders; rtype; body_def; notations}
@@ -427,10 +428,10 @@ GRAMMAR EXTEND Gram
| -> { [] }
] ]
;
- record_binder_body:
- [ [ l = binders; oc = of_type_with_opt_coercion;
+ field_body:
+ [ [ l = binders; oc = of_type;
t = lconstr -> { fun id -> (oc,AssumExpr (id,l,t)) }
- | l = binders; oc = of_type_with_opt_coercion;
+ | l = binders; oc = of_type;
t = lconstr; ":="; b = lconstr -> { fun id ->
(oc,DefExpr (id,l,b,Some t)) }
| l = binders; ":="; b = lconstr -> { fun id ->
@@ -442,22 +443,22 @@ GRAMMAR EXTEND Gram
;
record_binder:
[ [ id = name -> { (NoInstance,AssumExpr(id, [], CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) }
- | id = name; f = record_binder_body -> { f id } ] ]
+ | id = name; f = field_body -> { f id } ] ]
;
assum_list:
- [ [ bl = LIST1 assum_coe -> { bl } | b = simple_assum_coe -> { [b] } ] ]
+ [ [ bl = LIST1 assum_coe -> { bl } | b = assumpt -> { [b] } ] ]
;
assum_coe:
- [ [ "("; a = simple_assum_coe; ")" -> { a } ] ]
+ [ [ "("; a = assumpt; ")" -> { a } ] ]
;
- simple_assum_coe:
- [ [ idl = LIST1 ident_decl; oc = of_type_with_opt_coercion; c = lconstr ->
+ assumpt:
+ [ [ idl = LIST1 ident_decl; oc = of_type; c = lconstr ->
{ (oc <> NoInstance,(idl,c)) } ] ]
;
constructor_type:
[[ l = binders;
- t= [ coe = of_type_with_opt_coercion; c = lconstr ->
+ t= [ coe = of_type; c = lconstr ->
{ fun l id -> (coe <> NoInstance,(id,mkProdCN ~loc l c)) }
| ->
{ fun l id -> (false,(id,mkProdCN ~loc l (CAst.make ~loc @@ CHole (None, IntroAnonymous, None)))) } ]
@@ -468,7 +469,7 @@ GRAMMAR EXTEND Gram
constructor:
[ [ id = identref; c=constructor_type -> { c id } ] ]
;
- of_type_with_opt_coercion:
+ of_type:
[ [ ":>" -> { BackInstance }
| ":"; ">" -> { BackInstance }
| ":" -> { NoInstance } ] ]
@@ -687,7 +688,7 @@ GRAMMAR EXTEND Gram
{ VernacContext (List.flatten c) }
| IDENT "Instance"; namesup = instance_name; ":";
- t = operconstr LEVEL "200";
+ t = term LEVEL "200";
info = hint_info ;
props = [ ":="; "{"; r = record_declaration; "}" -> { Some (true,r) } |
":="; c = lconstr -> { Some (false,c) } | -> { None } ] ->
@@ -707,13 +708,13 @@ GRAMMAR EXTEND Gram
(* Arguments *)
| IDENT "Arguments"; qid = smart_global;
- args = LIST0 argument_spec_block;
+ args = LIST0 arg_specs;
more_implicits = OPT
[ ","; impl = LIST1
- [ impl = LIST0 more_implicits_block -> { List.flatten impl } ]
+ [ impl = LIST0 implicits_alt -> { List.flatten impl } ]
SEP "," -> { impl }
];
- mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> { l } ] ->
+ mods = OPT [ ":"; l = LIST1 args_modifier SEP "," -> { l } ] ->
{ let mods = match mods with None -> [] | Some l -> List.flatten l in
let more_implicits = Option.default [] more_implicits in
VernacArguments (qid, List.flatten args, more_implicits, mods) }
@@ -732,7 +733,7 @@ GRAMMAR EXTEND Gram
idl = LIST1 identref -> { Some idl } ] ->
{ VernacGeneralizable gen } ] ]
;
- arguments_modifier:
+ args_modifier:
[ [ IDENT "simpl"; IDENT "nomatch" -> { [`ReductionDontExposeCase] }
| IDENT "simpl"; IDENT "never" -> { [`ReductionNeverUnfold] }
| IDENT "default"; IDENT "implicits" -> { [`DefaultImplicits] }
@@ -757,7 +758,7 @@ GRAMMAR EXTEND Gram
]
];
(* List of arguments implicit status, scope, modifiers *)
- argument_spec_block: [
+ arg_specs: [
[ item = argument_spec ->
{ let name, recarg_like, notation_scope = item in
[RealArg { name=name; recarg_like=recarg_like;
@@ -791,8 +792,8 @@ GRAMMAR EXTEND Gram
implicit_status = MaxImplicit}) items }
]
];
- (* Same as [argument_spec_block], but with only implicit status and names *)
- more_implicits_block: [
+ (* Same as [arg_specs], but with only implicit status and names *)
+ implicits_alt: [
[ name = name -> { [(name.CAst.v, Explicit)] }
| "["; items = LIST1 name; "]" ->
{ List.map (fun name -> (name.CAst.v, NonMaxImplicit)) items }
@@ -826,9 +827,9 @@ GRAMMAR EXTEND Gram
GLOBAL: command query_command class_rawexpr gallina_ext search_query search_queries;
gallina_ext:
- [ [ IDENT "Export"; "Set"; table = option_table; v = option_setting ->
+ [ [ IDENT "Export"; "Set"; table = setting_name; v = option_setting ->
{ VernacSetOption (true, table, v) }
- | IDENT "Export"; IDENT "Unset"; table = option_table ->
+ | IDENT "Export"; IDENT "Unset"; table = setting_name ->
{ VernacSetOption (true, table, OptionUnset) }
] ];
@@ -837,7 +838,7 @@ GRAMMAR EXTEND Gram
(* Hack! Should be in grammar_ext, but camlp5 factorizes badly *)
| IDENT "Declare"; IDENT "Instance"; id = ident_decl; bl = binders; ":";
- t = operconstr LEVEL "200";
+ t = term LEVEL "200";
info = hint_info ->
{ VernacDeclareInstance (id, bl, t, info) }
@@ -885,12 +886,12 @@ GRAMMAR EXTEND Gram
{ VernacAddMLPath dir }
(* For acting on parameter tables *)
- | "Set"; table = option_table; v = option_setting ->
+ | "Set"; table = setting_name; v = option_setting ->
{ VernacSetOption (false, table, v) }
- | IDENT "Unset"; table = option_table ->
+ | IDENT "Unset"; table = setting_name ->
{ VernacSetOption (false, table, OptionUnset) }
- | IDENT "Print"; IDENT "Table"; table = option_table ->
+ | IDENT "Print"; IDENT "Table"; table = setting_name ->
{ VernacPrintOption table }
| IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 table_value
@@ -902,9 +903,9 @@ GRAMMAR EXTEND Gram
| IDENT "Add"; table = IDENT; v = LIST1 table_value ->
{ VernacAddOption ([table], v) }
- | IDENT "Test"; table = option_table; "for"; v = LIST1 table_value
+ | IDENT "Test"; table = setting_name; "for"; v = LIST1 table_value
-> { VernacMemOption (table, v) }
- | IDENT "Test"; table = option_table ->
+ | IDENT "Test"; table = setting_name ->
{ VernacPrintOption table }
| IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 table_value
@@ -1006,7 +1007,7 @@ GRAMMAR EXTEND Gram
[ [ id = global -> { Goptions.QualidRefValue id }
| s = STRING -> { Goptions.StringRefValue s } ] ]
;
- option_table:
+ setting_name:
[ [ fl = LIST1 [ x = IDENT -> { x } ] -> { fl } ]]
;
ne_in_or_out_modules:
@@ -1191,10 +1192,10 @@ GRAMMAR EXTEND Gram
| s, None -> SetFormat ("text",s) end }
| x = IDENT; ","; l = LIST1 [id = IDENT -> { id } ] SEP ","; "at";
lev = level -> { SetItemLevel (x::l,None,lev) }
- | x = IDENT; "at"; lev = level; b = OPT constr_as_binder_kind ->
+ | x = IDENT; "at"; lev = level; b = OPT binder_interp ->
{ SetItemLevel ([x],b,lev) }
- | x = IDENT; b = constr_as_binder_kind -> { SetItemLevel ([x],Some b,DefaultLevel) }
- | x = IDENT; typ = syntax_extension_type -> { SetEntryType (x,typ) }
+ | x = IDENT; b = binder_interp -> { SetItemLevel ([x],Some b,DefaultLevel) }
+ | x = IDENT; typ = explicit_subentry -> { SetEntryType (x,typ) }
] ]
;
syntax_modifiers:
@@ -1202,18 +1203,18 @@ GRAMMAR EXTEND Gram
| -> { [] }
] ]
;
- syntax_extension_type:
+ explicit_subentry:
[ [ IDENT "ident" -> { ETIdent } | IDENT "global" -> { ETGlobal }
| IDENT "bigint" -> { ETBigint }
| IDENT "binder" -> { ETBinder true }
| IDENT "constr" -> { ETConstr (InConstrEntry,None,DefaultLevel) }
- | IDENT "constr"; n = at_level_opt; b = OPT constr_as_binder_kind -> { ETConstr (InConstrEntry,b,n) }
+ | IDENT "constr"; n = at_level_opt; b = OPT binder_interp -> { ETConstr (InConstrEntry,b,n) }
| IDENT "pattern" -> { ETPattern (false,None) }
| IDENT "pattern"; "at"; IDENT "level"; n = natural -> { ETPattern (false,Some n) }
| IDENT "strict"; IDENT "pattern" -> { ETPattern (true,None) }
| IDENT "strict"; IDENT "pattern"; "at"; IDENT "level"; n = natural -> { ETPattern (true,Some n) }
| IDENT "closed"; IDENT "binder" -> { ETBinder false }
- | IDENT "custom"; x = IDENT; n = at_level_opt; b = OPT constr_as_binder_kind ->
+ | IDENT "custom"; x = IDENT; n = at_level_opt; b = OPT binder_interp ->
{ ETConstr (InCustomEntry x,b,n) }
] ]
;
@@ -1221,7 +1222,7 @@ GRAMMAR EXTEND Gram
[ [ "at"; n = level -> { n }
| -> { DefaultLevel } ] ]
;
- constr_as_binder_kind:
+ binder_interp:
[ [ "as"; IDENT "ident" -> { Notation_term.AsIdent }
| "as"; IDENT "pattern" -> { Notation_term.AsIdentOrPattern }
| "as"; IDENT "strict"; IDENT "pattern" -> { Notation_term.AsStrictPattern } ] ]
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 5f7eb78a40..bef9e29ac2 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -656,7 +656,7 @@ let explain_evar_not_found env sigma id =
let explain_wrong_case_info env (ind,u) ci =
let pi = pr_inductive env ind in
- if eq_ind ci.ci_ind ind then
+ if Ind.CanOrd.equal ci.ci_ind ind then
str "Pattern-matching expression on an object of inductive type" ++
spc () ++ pi ++ spc () ++ str "has invalid information."
else
@@ -1232,7 +1232,7 @@ let error_not_allowed_dependent_analysis env isrec i =
pr_inductive env i ++ str "."
let error_not_mutual_in_scheme env ind ind' =
- if eq_ind ind ind' then
+ if Ind.CanOrd.equal ind ind' then
str "The inductive type " ++ pr_inductive env ind ++
str " occurs twice."
else
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 356ccef06b..de72a30f18 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -405,7 +405,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort =
let get_common_underlying_mutual_inductive env = function
| [] -> assert false
| (id,(mind,i as ind))::l as all ->
- match List.filter (fun (_,(mind',_)) -> not (MutInd.equal mind mind')) l with
+ match List.filter (fun (_,(mind',_)) -> not (Environ.QMutInd.equal env mind mind')) l with
| (_,ind')::_ ->
raise (RecursionSchemeError (env, NotMutualInScheme (ind,ind')))
| [] ->
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 8ce59c40c3..185abcf35b 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -61,15 +61,15 @@ let pr_registered_grammar name =
prlist pr_one entries
let pr_grammar = function
- | "constr" | "operconstr" | "binder_constr" ->
+ | "constr" | "term" | "binder_constr" ->
str "Entry constr is" ++ fnl () ++
pr_entry Pcoq.Constr.constr ++
str "and lconstr is" ++ fnl () ++
pr_entry Pcoq.Constr.lconstr ++
str "where binder_constr is" ++ fnl () ++
pr_entry Pcoq.Constr.binder_constr ++
- str "and operconstr is" ++ fnl () ++
- pr_entry Pcoq.Constr.operconstr
+ str "and term is" ++ fnl () ++
+ pr_entry Pcoq.Constr.term
| "pattern" ->
pr_entry Pcoq.Constr.pattern
| "vernac" ->
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index 95680c2a4e..bdb0cabacf 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -18,30 +18,30 @@ module NamedDecl = Context.Named.Declaration
let known_names = Summary.ref [] ~name:"proofusing-nameset"
-let rec close_fwd e s =
+let rec close_fwd env sigma s =
let s' =
List.fold_left (fun s decl ->
let vb = match decl with
| LocalAssum _ -> Id.Set.empty
- | LocalDef (_,b,_) -> global_vars_set e b
+ | LocalDef (_,b,_) -> Termops.global_vars_set env sigma b
in
- let vty = global_vars_set e (NamedDecl.get_type decl) in
+ let vty = Termops.global_vars_set env sigma (NamedDecl.get_type decl) in
let vbty = Id.Set.union vb vty in
if Id.Set.exists (fun v -> Id.Set.mem v s) vbty
then Id.Set.add (NamedDecl.get_id decl) (Id.Set.union s vbty) else s)
- s (named_context e)
+ s (EConstr.named_context env)
in
- if Id.Set.equal s s' then s else close_fwd e s'
+ if Id.Set.equal s s' then s else close_fwd env sigma s'
-let set_of_type env ty =
+let set_of_type env sigma ty =
List.fold_left (fun acc ty ->
- Id.Set.union (global_vars_set env ty) acc)
+ Id.Set.union (Termops.global_vars_set env sigma ty) acc)
Id.Set.empty ty
let full_set env =
List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty
-let process_expr env e v_ty =
+let process_expr env sigma e v_ty =
let rec aux = function
| SsEmpty -> Id.Set.empty
| SsType -> v_ty
@@ -49,7 +49,7 @@ let process_expr env e v_ty =
| SsUnion(e1,e2) -> Id.Set.union (aux e1) (aux e2)
| SsSubstr(e1,e2) -> Id.Set.diff (aux e1) (aux e2)
| SsCompl e -> Id.Set.diff (full_set env) (aux e)
- | SsFwdClose e -> close_fwd env (aux e)
+ | SsFwdClose e -> close_fwd env sigma (aux e)
and set_of_id id =
if Id.to_string id = "All" then
full_set env
@@ -59,9 +59,9 @@ let process_expr env e v_ty =
in
aux e
-let process_expr env e ty =
- let v_ty = set_of_type env ty in
- let s = Id.Set.union v_ty (process_expr env e v_ty) in
+let process_expr env sigma e ty =
+ let v_ty = set_of_type env sigma ty in
+ let s = Id.Set.union v_ty (process_expr env sigma e v_ty) in
Id.Set.elements s
let name_set id expr = known_names := (id,expr) :: !known_names
@@ -110,7 +110,7 @@ let suggest_common env ppid used ids_typ skip =
S.empty (named_context env)
in
let all = S.diff all skip in
- let fwd_typ = close_fwd env ids_typ in
+ let fwd_typ = close_fwd env (Evd.from_env env) ids_typ in
if !Flags.debug then begin
print (str "All " ++ pr_set false all);
print (str "Type " ++ pr_set false ids_typ);
diff --git a/vernac/proof_using.mli b/vernac/proof_using.mli
index dfc233e8fa..93dbd33ae4 100644
--- a/vernac/proof_using.mli
+++ b/vernac/proof_using.mli
@@ -11,7 +11,8 @@
(** Utility code for section variables handling in Proof using... *)
val process_expr :
- Environ.env -> Vernacexpr.section_subset_expr -> Constr.types list ->
+ Environ.env -> Evd.evar_map ->
+ Vernacexpr.section_subset_expr -> EConstr.types list ->
Names.Id.t list
val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit
@@ -24,3 +25,5 @@ val get_default_proof_using : unit -> Vernacexpr.section_subset_expr option
val proof_using_opt_name : string list
(** For the stm *)
+
+val using_from_string : string -> Vernacexpr.section_subset_expr
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index c9f68eed57..a7de34dd09 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -43,7 +43,8 @@ module Vernac_ =
let command = Entry.create "command"
let syntax = Entry.create "syntax_command"
let vernac_control = Entry.create "Vernac.vernac_control"
- let rec_definition = Entry.create "Vernac.rec_definition"
+ let fix_definition = Entry.create "Vernac.fix_definition"
+ let rec_definition = fix_definition
let red_expr = Entry.create "red_expr"
let hint_info = Entry.create "hint_info"
(* Main vernac entry *)
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
index 8ab4af7d48..dac6877cb3 100644
--- a/vernac/pvernac.mli
+++ b/vernac/pvernac.mli
@@ -25,7 +25,9 @@ module Vernac_ :
val command : vernac_expr Entry.t
val syntax : vernac_expr Entry.t
val vernac_control : vernac_control Entry.t
+ val fix_definition : fixpoint_expr Entry.t
val rec_definition : fixpoint_expr Entry.t
+ [@@deprecated "Deprecated in 8.13; use 'fix_definition' instead"]
val noedit_mode : vernac_expr Entry.t
val command_entry : vernac_expr Entry.t
val main_entry : vernac_control option Entry.t
diff --git a/vernac/recLemmas.ml b/vernac/recLemmas.ml
index 534c358a3f..af72c01758 100644
--- a/vernac/recLemmas.ml
+++ b/vernac/recLemmas.ml
@@ -44,7 +44,7 @@ let find_mutually_recursive_statements sigma thms =
[] in
ind_hyps,ind_ccl) thms in
let inds_hyps,ind_ccls = List.split inds in
- let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> Names.MutInd.equal kn kn' in
+ let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> Environ.QMutInd.equal (Global.env ()) kn kn' in
(* Check if all conclusions are coinductive in the same type *)
(* (degenerated cartesian product since there is at most one coind ccl) *)
let same_indccl =
@@ -70,7 +70,7 @@ let find_mutually_recursive_statements sigma thms =
| [], _::_ ->
let () = match same_indccl with
| ind :: _ ->
- if List.distinct_f Names.ind_ord (List.map pi1 ind)
+ if List.distinct_f Names.Ind.CanOrd.compare (List.map pi1 ind)
then
Flags.if_verbose Feedback.msg_info
(Pp.strbrk
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 3ced38d6ea..bc03994ca6 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -57,14 +57,16 @@ module DefAttributes = struct
program : bool;
deprecated : Deprecation.t option;
canonical_instance : bool;
+ using : Vernacexpr.section_subset_expr option;
}
let parse f =
let open Attributes in
- let (((locality, deprecated), polymorphic), program), canonical_instance =
- parse Notations.(locality ++ deprecation ++ polymorphic ++ program ++ canonical_instance) f
+ let ((((locality, deprecated), polymorphic), program), canonical_instance), using =
+ parse Notations.(locality ++ deprecation ++ polymorphic ++ program ++ canonical_instance ++ using) f
in
- { polymorphic; program; locality; deprecated; canonical_instance }
+ let using = Option.map Proof_using.using_from_string using in
+ { polymorphic; program; locality; deprecated; canonical_instance; using }
end
let module_locality = Attributes.Notations.(locality >>= fun l -> return (make_module_locality l))
@@ -496,6 +498,25 @@ let program_inference_hook env sigma ev =
user_err Pp.(str "The statement obligations could not be resolved \
automatically, write a statement definition first.")
+let vernac_set_used_variables ~pstate e : Declare.Proof.t =
+ let env = Global.env () in
+ let sigma, _ = Declare.Proof.get_current_context pstate in
+ let initial_goals pf = Proofview.initial_goals Proof.((data pf).entry) in
+ let tys = List.map snd (initial_goals (Declare.Proof.get pstate)) in
+ let l = Proof_using.process_expr env sigma e tys in
+ let vars = Environ.named_context env in
+ List.iter (fun id ->
+ if not (List.exists (NamedDecl.get_id %> Id.equal id) vars) then
+ user_err ~hdr:"vernac_set_used_variables"
+ (str "Unknown variable: " ++ Id.print id))
+ l;
+ let _, pstate = Declare.Proof.set_used_variables pstate l in
+ pstate
+let vernac_set_used_variables_opt ?using pstate =
+ match using with
+ | None -> pstate
+ | Some expr -> vernac_set_used_variables ~pstate expr
+
(* XXX: Interpretation of lemma command, duplication with ComFixpoint
/ ComDefinition ? *)
let interp_lemma ~program_mode ~flags ~scope env0 evd thms =
@@ -525,7 +546,7 @@ let post_check_evd ~udecl ~poly evd =
else (* We fix the variables to ensure they won't be lowered to Set *)
Evd.fix_undefined_variables evd
-let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
+let start_lemma_com ~program_mode ~poly ~scope ~kind ?using ?hook thms =
let env0 = Global.env () in
let flags = Pretyping.{ all_no_fail_flags with program_mode } in
let decl = fst (List.hd thms) in
@@ -533,17 +554,20 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
let evd, thms = interp_lemma ~program_mode ~flags ~scope env0 evd thms in
let mut_analysis = RecLemmas.look_for_possibly_mutual_statements evd thms in
let evd = Evd.minimize_universes evd in
- match mut_analysis with
- | RecLemmas.NonMutual thm ->
- let thm = Declare.CInfo.to_constr evd thm in
- let evd = post_check_evd ~udecl ~poly evd in
- let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in
- Declare.Proof.start_with_initialization ~info ~cinfo:thm evd
- | RecLemmas.Mutual { mutual_info; cinfo ; possible_guards } ->
- let cinfo = List.map (Declare.CInfo.to_constr evd) cinfo in
- let evd = post_check_evd ~udecl ~poly evd in
- let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in
- Declare.Proof.start_mutual_with_initialization ~info ~cinfo evd ~mutual_info (Some possible_guards)
+ let pstate =
+ match mut_analysis with
+ | RecLemmas.NonMutual thm ->
+ let thm = Declare.CInfo.to_constr evd thm in
+ let evd = post_check_evd ~udecl ~poly evd in
+ let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in
+ Declare.Proof.start_with_initialization ~info ~cinfo:thm evd
+ | RecLemmas.Mutual { mutual_info; cinfo ; possible_guards } ->
+ let cinfo = List.map (Declare.CInfo.to_constr evd) cinfo in
+ let evd = post_check_evd ~udecl ~poly evd in
+ let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in
+ Declare.Proof.start_mutual_with_initialization ~info ~cinfo evd ~mutual_info (Some possible_guards)
+ in
+ vernac_set_used_variables_opt ?using pstate
let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in function
| Coercion ->
@@ -583,7 +607,7 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
let program_mode = atts.program in
let poly = atts.polymorphic in
let name = vernac_definition_name lid local in
- start_lemma_com ~program_mode ~poly ~scope:local ~kind:(Decls.IsDefinition kind) ?hook [(name, pl), (bl, t)]
+ start_lemma_com ~program_mode ~poly ~scope:local ~kind:(Decls.IsDefinition kind) ?using:atts.using ?hook [(name, pl), (bl, t)]
let vernac_definition ~atts ~pm (discharge, kind) (lid, pl) bl red_option c typ_opt =
let open DefAttributes in
@@ -604,7 +628,7 @@ let vernac_definition ~atts ~pm (discharge, kind) (lid, pl) bl red_option c typ_
else
let () =
ComDefinition.do_definition ~name:name.v
- ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook in
+ ~poly:atts.polymorphic ~scope ~kind ?using:atts.using pl bl red_option c typ_opt ?hook in
pm
(* NB: pstate argument to use combinators easily *)
@@ -613,7 +637,7 @@ let vernac_start_proof ~atts kind l =
let scope = enforce_locality_exp atts.locality NoDischarge in
if Dumpglob.dump () then
List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l;
- start_lemma_com ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Decls.IsProof kind) l
+ start_lemma_com ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Decls.IsProof kind) ?using:atts.using l
let vernac_end_proof ~lemma ~pm = let open Vernacexpr in function
| Admitted ->
@@ -639,6 +663,8 @@ let vernac_assumption ~atts discharge kind l nl =
match scope with
| Global _ -> Dumpglob.dump_definition lid false "ax"
| Discharge -> Dumpglob.dump_definition lid true "var") idl) l;
+ if Option.has_some atts.using then
+ Attributes.unsupported_attributes ["using",VernacFlagEmpty];
ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l
let is_polymorphic_inductive_cumulativity =
@@ -842,16 +868,17 @@ let vernac_fixpoint_interactive ~atts discharge l =
let scope = vernac_fixpoint_common ~atts discharge l in
if atts.program then
CErrors.user_err Pp.(str"Program Fixpoint requires a body");
- ComFixpoint.do_fixpoint_interactive ~scope ~poly:atts.polymorphic l
+ vernac_set_used_variables_opt ?using:atts.using
+ (ComFixpoint.do_fixpoint_interactive ~scope ~poly:atts.polymorphic l)
let vernac_fixpoint ~atts ~pm discharge l =
let open DefAttributes in
let scope = vernac_fixpoint_common ~atts discharge l in
if atts.program then
(* XXX: Switch to the attribute system and match on ~atts *)
- ComProgramFixpoint.do_fixpoint ~pm ~scope ~poly:atts.polymorphic l
+ ComProgramFixpoint.do_fixpoint ~pm ~scope ~poly:atts.polymorphic ?using:atts.using l
else
- let () = ComFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic l in
+ let () = ComFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic ?using:atts.using l in
pm
let vernac_cofixpoint_common ~atts discharge l =
@@ -864,15 +891,16 @@ let vernac_cofixpoint_interactive ~atts discharge l =
let scope = vernac_cofixpoint_common ~atts discharge l in
if atts.program then
CErrors.user_err Pp.(str"Program CoFixpoint requires a body");
- ComFixpoint.do_cofixpoint_interactive ~scope ~poly:atts.polymorphic l
+ vernac_set_used_variables_opt ?using:atts.using
+ (ComFixpoint.do_cofixpoint_interactive ~scope ~poly:atts.polymorphic l)
let vernac_cofixpoint ~atts ~pm discharge l =
let open DefAttributes in
let scope = vernac_cofixpoint_common ~atts discharge l in
if atts.program then
- ComProgramFixpoint.do_cofixpoint ~pm ~scope ~poly:atts.polymorphic l
+ ComProgramFixpoint.do_cofixpoint ~pm ~scope ~poly:atts.polymorphic ?using:atts.using l
else
- let () = ComFixpoint.do_cofixpoint ~scope ~poly:atts.polymorphic l in
+ let () = ComFixpoint.do_cofixpoint ~scope ~poly:atts.polymorphic ?using:atts.using l in
pm
let vernac_scheme l =
@@ -1223,21 +1251,6 @@ let vernac_set_end_tac ~pstate tac =
(* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
Declare.Proof.set_endline_tactic tac pstate
-let vernac_set_used_variables ~pstate e : Declare.Proof.t =
- let env = Global.env () in
- let initial_goals pf = Proofview.initial_goals Proof.(data pf).Proof.entry in
- let tys = List.map snd (initial_goals (Declare.Proof.get pstate)) in
- let tys = List.map EConstr.Unsafe.to_constr tys in
- let l = Proof_using.process_expr env e tys in
- let vars = Environ.named_context env in
- List.iter (fun id ->
- if not (List.exists (NamedDecl.get_id %> Id.equal id) vars) then
- user_err ~hdr:"vernac_set_used_variables"
- (str "Unknown variable: " ++ Id.print id))
- l;
- let _, pstate = Declare.Proof.set_used_variables pstate l in
- pstate
-
(*****************************)
(* Auxiliary file management *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 18:28:33 +0000