aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/subtac/subtac_classes.ml2
-rw-r--r--contrib/subtac/subtac_obligations.ml2
-rw-r--r--library/impargs.ml8
-rw-r--r--library/impargs.mli6
-rw-r--r--toplevel/classes.ml6
-rw-r--r--toplevel/command.ml14
-rw-r--r--toplevel/record.ml3
-rw-r--r--toplevel/vernacentries.ml2
8 files changed, 22 insertions, 21 deletions
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index e966c3afc..289e64c29 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -186,7 +186,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
let hook gr =
let cst = match gr with ConstRef kn -> kn | _ -> assert false in
let inst = Typeclasses.new_instance k pri global cst in
- Impargs.declare_manual_implicits false gr false imps;
+ Impargs.declare_manual_implicits false gr ~enriching:false imps;
Typeclasses.add_instance inst
in
let evm = Subtac_utils.evars_of_term (Evd.evars_of !isevars) Evd.empty term in
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 6d1ec5ede..ce75299de 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -198,7 +198,7 @@ let declare_definition prg =
in
let gr = ConstRef c in
if Impargs.is_implicit_args () || prg.prg_implicits <> [] then
- Impargs.declare_manual_implicits false gr (Impargs.is_implicit_args ()) prg.prg_implicits;
+ Impargs.declare_manual_implicits false gr prg.prg_implicits;
print_message (Subtac_utils.definition_message prg.prg_name);
prg.prg_hook gr;
gr
diff --git a/library/impargs.ml b/library/impargs.ml
index bb11ce2f8..b477d9495 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -71,6 +71,7 @@ let make_maximal_implicit_args flag =
let is_implicit_args () = !implicit_args.main
let is_manual_implicit_args () = !implicit_args.manual
+let is_auto_implicit_args () = !implicit_args.main && not (is_manual_implicit_args ())
let is_strict_implicit_args () = !implicit_args.strict
let is_strongly_strict_implicit_args () = !implicit_args.strongly_strict
let is_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern
@@ -577,10 +578,11 @@ type manual_explicitation = Topconstr.explicitation * (bool * bool)
let compute_implicits_with_manual env typ enriching l =
compute_manual_implicits env !implicit_args typ enriching l
-let declare_manual_implicits local ref enriching l =
+let declare_manual_implicits local ref ?enriching l =
let flags = !implicit_args in
let env = Global.env () in
let t = Global.type_of_global ref in
+ let enriching = Option.default (is_auto_implicit_args ()) enriching in
let l' = compute_manual_implicits env flags t enriching l in
let req =
if local or isVarRef ref then ImplLocal
@@ -588,9 +590,9 @@ let declare_manual_implicits local ref enriching l =
in
add_anonymous_leaf (inImplicits (req,[ref,l']))
-let maybe_declare_manual_implicits local ref enriching l =
+let maybe_declare_manual_implicits local ref ?enriching l =
if l = [] then ()
- else declare_manual_implicits local ref enriching l
+ else declare_manual_implicits local ref ?enriching l
let lift_implicits n =
List.map (fun x ->
diff --git a/library/impargs.mli b/library/impargs.mli
index 353f657c6..0eba9f380 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -83,14 +83,16 @@ val declare_implicits : bool -> global_reference -> unit
(* [declare_manual_implicits local ref enriching l]
Manual declaration of which arguments are expected implicit.
+ If not set, we decide if it should enrich by automatically inferd
+ implicits depending on the current state.
Unsets implicits if [l] is empty. *)
-val declare_manual_implicits : bool -> global_reference -> bool ->
+val declare_manual_implicits : bool -> global_reference -> ?enriching:bool ->
manual_explicitation list -> unit
(* If the list is empty, do nothing, otherwise declare the implicits. *)
-val maybe_declare_manual_implicits : bool -> global_reference -> bool ->
+val maybe_declare_manual_implicits : bool -> global_reference -> ?enriching:bool ->
manual_explicitation list -> unit
val implicits_of_global : global_reference -> implicits_list
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index f63ae3ecb..4a8ce920f 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -230,8 +230,8 @@ let new_class id par ar sup props =
(DefinitionEntry proj_entry, IsDefinition Definition)
in
let cref = ConstRef cst in
- Impargs.declare_manual_implicits false cref (Impargs.is_implicit_args()) arity_imps;
- Impargs.declare_manual_implicits false (ConstRef proj_cst) (Impargs.is_implicit_args()) (List.hd fieldimpls);
+ Impargs.declare_manual_implicits false cref arity_imps;
+ Impargs.declare_manual_implicits false (ConstRef proj_cst) (List.hd fieldimpls);
set_rigid cst;
cref, [proj_name, Some proj_cst]
| _ ->
@@ -321,7 +321,7 @@ let fail_on_free_vars = function
let instance_hook k pri global imps ?hook cst =
let inst = Typeclasses.new_instance k pri global cst in
- Impargs.maybe_declare_manual_implicits false (ConstRef cst) false imps;
+ Impargs.maybe_declare_manual_implicits false (ConstRef cst) ~enriching:false imps;
Typeclasses.add_instance inst;
(match hook with Some h -> h cst | None -> ())
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 9ae3f8e82..c8acd8113 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -136,7 +136,7 @@ let red_constant_entry bl ce = function
let declare_global_definition ident ce local imps =
let kn = declare_constant ident (DefinitionEntry ce,IsDefinition Definition) in
let gr = ConstRef kn in
- maybe_declare_manual_implicits false gr (is_implicit_args ()) imps;
+ maybe_declare_manual_implicits false gr imps;
if local = Local && Flags.is_verbose() then
msg_warning (pr_id ident ++ str" is declared as a global definition");
definition_message ident;
@@ -189,7 +189,7 @@ let declare_one_assumption is_coe (local,kind) c imps impl keep nl (_,ident) =
let kn =
declare_constant ident (ParameterEntry (c,nl), IsAssumption kind) in
let gr = ConstRef kn in
- maybe_declare_manual_implicits false gr (is_implicit_args ()) imps;
+ maybe_declare_manual_implicits false gr imps;
assumption_message ident;
if local=Local & Flags.is_verbose () then
msg_warning (pr_id ident ++ str" is declared as a parameter" ++
@@ -625,12 +625,10 @@ let declare_mutual_with_eliminations isrecord mie impls =
let (_,kn) = declare_mind isrecord mie in
list_iter_i (fun i (indimpls, constrimpls) ->
let ind = (kn,i) in
- maybe_declare_manual_implicits false (IndRef ind)
- (is_implicit_args()) indimpls;
+ maybe_declare_manual_implicits false (IndRef ind) indimpls;
list_iter_i
(fun j impls ->
- maybe_declare_manual_implicits false (ConstructRef (ind, succ j))
- (is_implicit_args()) impls)
+ maybe_declare_manual_implicits false (ConstructRef (ind, succ j)) impls)
constrimpls)
impls;
if_verbose ppnl (minductive_message names);
@@ -785,7 +783,7 @@ let declare_fix boxed kind f def t imps =
} in
let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in
let gr = ConstRef kn in
- maybe_declare_manual_implicits false gr (is_implicit_args ()) imps;
+ maybe_declare_manual_implicits false gr imps;
gr
let prepare_recursive_declaration fixnames fixtypes fixdefs =
@@ -1209,7 +1207,7 @@ let start_proof_com kind thms hook =
list_map_i (save_remaining_recthms kind body opaq) 1 other_thms in
let thms_data = (strength,ref,imps)::other_thms_data in
List.iter (fun (strength,ref,imps) ->
- maybe_declare_manual_implicits false ref (is_implicit_args ()) imps;
+ maybe_declare_manual_implicits false ref imps;
hook strength ref) thms_data in
start_proof id kind t ?init_tac:rec_tac hook
diff --git a/toplevel/record.ml b/toplevel/record.ml
index ae97a8db4..8ac103fba 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -198,8 +198,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
raise (NotDefinable (BadTypedProj (fid,ctx,te))) in
let refi = ConstRef kn in
let constr_fi = mkConst kn in
- Impargs.maybe_declare_manual_implicits
- false refi (Impargs.is_implicit_args()) impls;
+ Impargs.maybe_declare_manual_implicits false refi impls;
if coe then begin
let cl = Class.class_of_global (IndRef indsp) in
Class.try_add_new_coercion_with_source refi Global cl
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 399c18c92..8f2d3c1e3 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -751,7 +751,7 @@ let vernac_syntactic_definition lid =
let vernac_declare_implicits local r = function
| Some imps ->
- Impargs.declare_manual_implicits local (global_with_alias r) false
+ Impargs.declare_manual_implicits local (global_with_alias r) ~enriching:false
(List.map (fun (ex,b,f) -> ex, (b,f)) imps)
| None ->
Impargs.declare_implicits local (global_with_alias r)
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 03:36:14 +0000