aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/comDefinition.ml16
-rw-r--r--vernac/comFixpoint.ml11
-rw-r--r--vernac/comProgramFixpoint.ml12
-rw-r--r--vernac/declare.ml7
-rw-r--r--vernac/declare.mli4
-rw-r--r--vernac/proof_using.ml23
-rw-r--r--vernac/proof_using.mli15
-rw-r--r--vernac/vernacentries.ml36
8 files changed, 68 insertions, 56 deletions
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index b3ffb864f2..2e48313630 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -111,6 +111,10 @@ 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 definition_using env evd ~body ~types ~using =
+ let terms = Option.List.cons types [body] in
+ Option.map (fun using -> Proof_using.definition_using env evd ~using ~terms) using
+
let do_definition ?hook ~name ~scope ~poly ?typing_flags ~kind ?using udecl bl red_option c ctypopt =
let program_mode = false in
let env = Global.env() in
@@ -120,11 +124,7 @@ let do_definition ?hook ~name ~scope ~poly ?typing_flags ~kind ?using udecl bl r
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 using = definition_using env evd ~body ~types ~using in
let kind = Decls.IsDefinition kind in
let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types ?using () in
let info = Declare.Info.make ~scope ~kind ?hook ~udecl ~poly ?typing_flags () in
@@ -141,11 +141,7 @@ let do_definition_program ?hook ~pm ~name ~scope ~poly ?typing_flags ~kind ?usin
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 using = definition_using env evd ~body ~types ~using 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 ?using () in
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 0cf0b07822..0f817ffbd1 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -259,13 +259,10 @@ let build_recthms ~indexes ?using fixnames fixtypes fiximps =
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 env = Global.env() in
+ let evd = Evd.from_env env in
+ let terms = [EConstr.of_constr typ] in
+ let using = Option.map (fun using -> Proof_using.definition_using env evd ~using ~terms) using in
let args = List.map Context.Rel.Declaration.get_name ctx in
Declare.CInfo.make ~name ~typ ~args ~impargs ?using ()
) fixnames fixtypes fiximps
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 3c4a651cf5..0651f3330e 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -259,10 +259,9 @@ let build_wellfounded pm (recname,pl,bl,arityc,body) poly ?typing_flags ?using r
let evars, _, evars_def, evars_typ =
RetrieveObl.retrieve_obligations env recname sigma 0 def typ
in
- let using = using |> Option.map (fun expr ->
+ let using =
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))
+ Option.map (fun using -> Proof_using.definition_using env sigma ~using ~terms) using
in
let uctx = Evd.evar_universe_context sigma in
let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ ?using () in
@@ -294,11 +293,8 @@ let do_program_recursive ~pm ~scope ~poly ?typing_flags ?using 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 terms = [def; typ] in
+ let using = Option.map (fun using -> Proof_using.definition_using env evd ~using ~terms) using 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
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 48aa329e5e..607ba18a95 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -57,7 +57,7 @@ module CInfo = struct
(** Names to pre-introduce *)
; impargs : Impargs.manual_implicits
(** Explicitily declared implicit arguments *)
- ; using : Names.Id.Set.t option
+ ; using : Proof_using.t option
(** Explicit declaration of section variables used by the constant *)
}
@@ -1478,11 +1478,10 @@ let start_mutual_with_initialization ~info ~cinfo ~mutual_info sigma snl =
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 =
+let set_used_variables ps ~using =
let open Context.Named.Declaration in
let env = Global.env () in
- let ids = List.fold_right Id.Set.add l Id.Set.empty in
- let ctx = Environ.keep_hyps env ids in
+ let ctx = Environ.keep_hyps env using in
let ctx_set =
List.fold_right Id.Set.add (List.map NamedDecl.get_id ctx) Id.Set.empty in
let vars_of = Environ.global_vars_set in
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 37a61cc4f0..81558e6f6b 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -79,7 +79,7 @@ module CInfo : sig
-> typ:'constr
-> ?args:Name.t list
-> ?impargs:Impargs.manual_implicits
- -> ?using:Names.Id.Set.t
+ -> ?using:Proof_using.t
-> unit
-> 'constr t
@@ -244,7 +244,7 @@ module Proof : sig
(** Sets the section variables assumed by the proof, returns its closure
* (w.r.t. type dependencies and let-ins covered by it) *)
- val set_used_variables : t -> Names.Id.t list -> Constr.named_context * t
+ val set_used_variables : t -> using:Proof_using.t -> 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 *)
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index bdb0cabacf..01e7b7cc3d 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -64,6 +64,12 @@ let process_expr env sigma e ty =
let s = Id.Set.union v_ty (process_expr env sigma e v_ty) in
Id.Set.elements s
+type t = Names.Id.Set.t
+
+let definition_using env evd ~using ~terms =
+ let l = process_expr env evd using terms in
+ Names.Id.Set.(List.fold_right add l empty)
+
let name_set id expr = known_names := (id,expr) :: !known_names
let minimize_hyps env ids =
@@ -91,13 +97,14 @@ let remove_ids_and_lets env s ids =
let record_proof_using expr =
Aux_file.record_in_aux "suggest_proof_using" expr
+let debug_proof_using = CDebug.create ~name:"proof-using" ()
+
(* Variables in [skip] come from after the definition, so don't count
for "All". Used in the variable case since the env contains the
variable itself. *)
let suggest_common env ppid used ids_typ skip =
let module S = Id.Set in
let open Pp in
- let print x = Feedback.msg_debug x in
let pr_set parens s =
let wrap ppcmds =
if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")"
@@ -111,13 +118,13 @@ let suggest_common env ppid used ids_typ skip =
in
let all = S.diff all skip 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);
- print (str "needed " ++ pr_set false needed);
- print (str "all_needed " ++ pr_set false all_needed);
- print (str "Type* " ++ pr_set false fwd_typ);
- end;
+ let () = debug_proof_using (fun () ->
+ str "All " ++ pr_set false all ++ fnl() ++
+ str "Type " ++ pr_set false ids_typ ++ fnl() ++
+ str "needed " ++ pr_set false needed ++ fnl() ++
+ str "all_needed " ++ pr_set false all_needed ++ fnl() ++
+ str "Type* " ++ pr_set false fwd_typ)
+ in
let valid_exprs = ref [] in
let valid e = valid_exprs := e :: !valid_exprs in
if S.is_empty needed then valid (str "Type");
diff --git a/vernac/proof_using.mli b/vernac/proof_using.mli
index 93dbd33ae4..60db4d60e6 100644
--- a/vernac/proof_using.mli
+++ b/vernac/proof_using.mli
@@ -10,10 +10,17 @@
(** Utility code for section variables handling in Proof using... *)
-val process_expr :
- Environ.env -> Evd.evar_map ->
- Vernacexpr.section_subset_expr -> EConstr.types list ->
- Names.Id.t list
+(** At some point it would be good to make this abstract *)
+type t = Names.Id.Set.t
+
+(** Process a [using] expression in definitions to provide the list of
+ used terms *)
+val definition_using
+ : Environ.env
+ -> Evd.evar_map
+ -> using:Vernacexpr.section_subset_expr
+ -> terms:EConstr.constr list
+ -> t
val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 664c6b2f36..38ca836b32 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -563,19 +563,19 @@ 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 vernac_set_used_variables ~pstate using : 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 terms = List.map snd (initial_goals (Declare.Proof.get pstate)) in
+ let using = Proof_using.definition_using env sigma ~using ~terms 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
+ Names.Id.Set.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))
+ using;
+ let _, pstate = Declare.Proof.set_used_variables pstate ~using in
pstate
let vernac_set_used_variables_opt ?using pstate =
@@ -1438,7 +1438,10 @@ let vernac_reserve bl =
let env = Global.env() in
let sigma = Evd.from_env env in
let t,ctx = Constrintern.interp_type env sigma c in
- let t = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_ctx ctx) t in
+ let t = Flags.without_option Detyping.print_universes (fun () ->
+ Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_ctx ctx) t)
+ ()
+ in
let t,_ = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in
Reserve.declare_reserved_type idl t)
in List.iter sb_decl bl
@@ -1642,6 +1645,13 @@ let () =
optwrite = CWarnings.set_flags }
let () =
+ declare_string_option
+ { optdepr = false;
+ optkey = ["Debug"];
+ optread = CDebug.get_flags;
+ optwrite = CDebug.set_flags }
+
+let () =
declare_bool_option
{ optdepr = false;
optkey = ["Guard"; "Checking"];
@@ -1707,9 +1717,9 @@ let vernac_set_append_option ~locality key s =
let vernac_set_option ~locality table v = match v with
| OptionSetString s ->
- (* We make a special case for warnings because appending is their
- natural semantics *)
- if CString.List.equal table ["Warnings"] then
+ (* We make a special case for warnings and debug flags because appending is
+ their natural semantics *)
+ if CString.List.equal table ["Warnings"] || CString.List.equal table ["Debug"] then
vernac_set_append_option ~locality table s
else
let (last, prefix) = List.sep_last table in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:03:57 +0000