aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/notation.ml2
-rw-r--r--library/declare.ml12
-rw-r--r--library/heads.ml2
-rw-r--r--library/impargs.ml96
-rw-r--r--library/impargs.mli43
-rw-r--r--library/lib.ml37
-rw-r--r--library/lib.mli11
-rw-r--r--library/libobject.ml14
-rw-r--r--library/libobject.mli6
-rw-r--r--pretyping/typeclasses.ml6
-rw-r--r--test-suite/success/ImplicitArguments.v2
-rw-r--r--toplevel/classes.ml14
-rw-r--r--toplevel/vernacentries.ml8
13 files changed, 179 insertions, 74 deletions
diff --git a/interp/notation.ml b/interp/notation.ml
index 164423ead..46089245c 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -467,7 +467,7 @@ let discharge_arguments_scope (_,(req,r,l)) =
if req = ArgsScopeNoDischarge or (isVarRef r & Lib.is_in_section r) then None
else Some (req,Lib.discharge_global r,l)
-let rebuild_arguments_scope (_,(req,r,l)) =
+let rebuild_arguments_scope (req,r,l) =
match req with
| ArgsScopeNoDischarge -> assert false
| ArgsScopeAuto ->
diff --git a/library/declare.ml b/library/declare.ml
index b524639ef..e250ec282 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -57,10 +57,12 @@ let cache_variable ((sp,_),o) =
let impl,opaq,cst,keep = match d with (* Fails if not well-typed *)
| SectionLocalAssum (ty, impl, keep) ->
let cst = Global.push_named_assum (id,ty) in
- impl, true, cst, (if keep then Some ty else None)
+ let impl = if impl then Rawterm.Implicit else Rawterm.Explicit in
+ let keep = if keep then Some ty else None in
+ impl, true, cst, keep
| SectionLocalDef (c,t,opaq) ->
let cst = Global.push_named_def (id,c,t) in
- false, opaq, cst, None in
+ Rawterm.Explicit, opaq, cst, None in
Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
add_section_variable id impl keep;
Dischargedhypsmap.set_discharged_hyps sp [];
@@ -116,7 +118,7 @@ let cache_constant ((sp,kn),(cdt,dhyps,kind)) =
let discharged_hyps kn sechyps =
let (_,dir,_) = repr_kn kn in
- let args = array_map_to_list destVar (instance_from_named_context sechyps) in
+ let args = Array.to_list (instance_from_variable_context sechyps) in
List.rev (List.map (Libnames.make_path dir) args)
let discharge_constant ((sp,kn),(cdt,dhyps,kind)) =
@@ -124,7 +126,7 @@ let discharge_constant ((sp,kn),(cdt,dhyps,kind)) =
let cb = Global.lookup_constant con in
let repl = replacement_context () in
let sechyps = section_segment_of_constant con in
- let recipe = { d_from=cb; d_modlist=repl; d_abstract=sechyps } in
+ let recipe = { d_from=cb; d_modlist=repl; d_abstract=named_of_variable_context sechyps } in
Some (GlobalRecipe recipe,(discharged_hyps kn sechyps)@dhyps,kind)
(* Hack to reduce the size of .vo: we keep only what load/open needs *)
@@ -235,7 +237,7 @@ let discharge_inductive ((sp,kn),(dhyps,mie)) =
let repl = replacement_context () in
let sechyps = section_segment_of_mutual_inductive kn in
Some (discharged_hyps kn sechyps,
- Discharge.process_inductive sechyps repl mie)
+ Discharge.process_inductive (named_of_variable_context sechyps) repl mie)
let dummy_one_inductive_entry mie = {
mind_entry_typename = mie.mind_entry_typename;
diff --git a/library/heads.ml b/library/heads.ml
index ca1f1014f..1b1dba43f 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -158,7 +158,7 @@ let discharge_head (_,(ref,k)) =
| EvalConstRef cst -> Some (EvalConstRef (pop_con cst), k)
| EvalVarRef id -> None
-let rebuild_head (info,(ref,k)) =
+let rebuild_head (ref,k) =
(ref, compute_head ref)
let export_head o = Some o
diff --git a/library/impargs.ml b/library/impargs.ml
index b5c27f430..4759ced46 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -27,6 +27,7 @@ open Topconstr
type implicits_flags = {
main : bool;
+ manual : bool; (* automatic or manual only *)
strict : bool; (* true = strict *)
strongly_strict : bool; (* true = strongly strict *)
reversible_pattern : bool;
@@ -38,6 +39,7 @@ type implicits_flags = {
let implicit_args = ref {
main = false;
+ manual = false;
strict = true;
strongly_strict = false;
reversible_pattern = false;
@@ -48,6 +50,10 @@ let implicit_args = ref {
let make_implicit_args flag =
implicit_args := { !implicit_args with main = flag }
+let make_manual_implicit_args flag =
+ implicit_args := { !implicit_args with main = if flag then true else !implicit_args.main;
+ manual = flag }
+
let make_strict_implicit_args flag =
implicit_args := { !implicit_args with strict = flag }
@@ -64,6 +70,7 @@ let make_maximal_implicit_args flag =
implicit_args := { !implicit_args with maximal = flag }
let is_implicit_args () = !implicit_args.main
+let is_manual_implicit_args () = !implicit_args.manual
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
@@ -245,10 +252,6 @@ let compute_implicits_flags env f all t =
let set_implicit id imp insmax =
(id,(match imp with None -> Manual | Some imp -> imp),insmax)
-let merge_imps f = function
- None -> Some Manual
- | x -> x
-
let rec assoc_by_pos k = function
(ExplByPos (k', x), b) :: tl when k = k' -> (x,b), tl
| hd :: tl -> let (x, tl) = assoc_by_pos k tl in x, hd :: tl
@@ -307,11 +310,15 @@ let compute_manual_implicits env flags t enriching l =
in
merge 1 l autoimps
+let const v _ = v
+
let compute_implicits_auto env f manual t =
match manual with
- [] -> let l = compute_implicits_flags env f false t in
- prepare_implicits f l
- | _ -> compute_manual_implicits env f t true manual
+ | [] ->
+ let l = compute_implicits_flags env f false t in
+ if f.manual then List.map (const None) l
+ else prepare_implicits f l
+ | _ -> compute_manual_implicits env f t (not f.manual) manual
let compute_implicits env t = compute_implicits_auto env !implicit_args [] t
@@ -415,12 +422,18 @@ let list_split_at index l =
| [] -> failwith "list_split_at: Invalid argument"
in aux 0 [] l
-let merge_impls newimpls oldimpls =
- let before, after = list_split_at (List.length newimpls - List.length oldimpls) newimpls in
+let merge_impls oldimpls newimpls =
+ let (before, news), olds =
+ let len = List.length newimpls - List.length oldimpls in
+ if len >= 0 then list_split_at len newimpls, oldimpls
+ else
+ let before, after = list_split_at (-len) oldimpls in
+ (before, newimpls), after
+ in
before @ (List.map2 (fun orig ni ->
match orig with
| Some (_, Manual, _) -> orig
- | _ -> ni) oldimpls after)
+ | _ -> ni) olds news)
(* Caching implicits *)
@@ -454,34 +467,67 @@ let subst_implicits_decl subst (r,imps as o) =
let subst_implicits (_,subst,(req,l)) =
(ImplLocal,list_smartmap (subst_implicits_decl subst) l)
+let impls_of_context ctx =
+ List.rev_map (fun (id,impl,_,_) -> if impl = Rawterm.Implicit then Some (id, Manual, true) else None)
+ (List.filter (fun (_,_,b,_) -> b = None) ctx)
+
+let section_segment_of_reference = function
+ | ConstRef con -> section_segment_of_constant con
+ | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
+ section_segment_of_mutual_inductive kn
+ | _ -> []
+
let discharge_implicits (_,(req,l)) =
match req with
| ImplLocal -> None
| ImplInteractive (ref,flags,exp) ->
- Some (ImplInteractive (pop_global_reference ref,flags,exp),l)
+ let vars = section_segment_of_reference ref in
+ let ref' = pop_global_reference ref in
+ let l' = [ref', impls_of_context vars @ snd (List.hd l)] in
+ Some (ImplInteractive (ref',flags,exp),l')
| ImplConstant (con,flags) ->
- Some (ImplConstant (pop_con con,flags),l)
+ let con' = pop_con con in
+ let l' = [ConstRef con',impls_of_context (section_segment_of_constant con) @ snd (List.hd l)] in
+ Some (ImplConstant (con',flags),l')
| ImplMutualInductive (kn,flags) ->
- Some (ImplMutualInductive (pop_kn kn,flags),l)
+ let l' = List.map (fun (gr, l) ->
+ let vars = section_segment_of_reference gr in
+ (pop_global_reference gr, impls_of_context vars @ l)) l
+ in
+ Some (ImplMutualInductive (pop_kn kn,flags),l')
-let rebuild_implicits (info,(req,l)) =
- let manual = List.fold_left (fun acc (id, impl, keep) ->
- if impl then (ExplByName id, (true, true)) :: acc else acc)
- [] info
- in
+let rebuild_implicits (req,l) =
let l' = match req with
| ImplLocal -> assert false
| ImplConstant (con,flags) ->
- [ConstRef con, compute_constant_implicits flags manual con]
+ let oldimpls = snd (List.hd l) in
+ let newimpls = compute_constant_implicits flags [] con in
+ [ConstRef con, merge_impls oldimpls newimpls]
| ImplMutualInductive (kn,flags) ->
- compute_all_mib_implicits flags manual kn
+ let newimpls = compute_all_mib_implicits flags [] kn in
+ let rec aux olds news =
+ match olds, news with
+ | (_, oldimpls) :: old, (gr, newimpls) :: tl ->
+ (gr, merge_impls oldimpls newimpls) :: aux old tl
+ | [], [] -> []
+ | _, _ -> assert false
+ in aux l newimpls
+
| ImplInteractive (ref,flags,o) ->
match o with
- | ImplAuto -> [ref,compute_global_implicits flags manual ref]
- | ImplManual l ->
- let auto = compute_global_implicits flags manual ref in
-(* let auto = if flags.main then auto else List.map (fun _ -> None) auto in *)
- let l' = merge_impls auto l in [ref,l']
+ | ImplAuto ->
+ let oldimpls = snd (List.hd l) in
+ let newimpls = compute_global_implicits flags [] ref in
+ [ref,merge_impls oldimpls newimpls]
+ | ImplManual m ->
+ let oldimpls = snd (List.hd l) in
+ let auto =
+ if flags.main then
+ let newimpls = compute_global_implicits flags [] ref in
+ merge_impls oldimpls newimpls
+ else oldimpls
+ in
+ let l' = merge_impls auto m in [ref,l']
in (req,l')
let export_implicits (req,_ as x) =
diff --git a/library/impargs.mli b/library/impargs.mli
index 5bfa0470d..353f657c6 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -20,6 +20,7 @@ open Nametab
are outside the kernel, which knows nothing about implicit arguments. *)
val make_implicit_args : bool -> unit
+val make_manual_implicit_args : bool -> unit
val make_strict_implicit_args : bool -> unit
val make_strongly_strict_implicit_args : bool -> unit
val make_reversible_pattern_implicit_args : bool -> unit
@@ -27,6 +28,7 @@ val make_contextual_implicit_args : bool -> unit
val make_maximal_implicit_args : bool -> unit
val is_implicit_args : unit -> bool
+val is_manual_implicit_args : unit -> bool
val is_strict_implicit_args : unit -> bool
val is_strongly_strict_implicit_args : unit -> bool
val is_reversible_pattern_implicit_args : unit -> bool
@@ -38,10 +40,20 @@ val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b
(*s An [implicits_list] is a list of positions telling which arguments
of a reference can be automatically infered *)
-type implicit_status
-type implicits_list = implicit_status list
-type implicit_explanation
+
+type argument_position =
+ | Conclusion
+ | Hyp of int
+
+type implicit_explanation =
+ | DepRigid of argument_position
+ | DepFlex of argument_position
+ | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position
+ | Manual
+
+type implicit_status = (identifier * implicit_explanation * bool) option
+type implicits_list = implicit_status list
val is_status_implicit : implicit_status -> bool
val is_inferable_implicit : bool -> int -> implicit_status -> bool
@@ -84,3 +96,28 @@ val maybe_declare_manual_implicits : bool -> global_reference -> bool ->
val implicits_of_global : global_reference -> implicits_list
val lift_implicits : int -> manual_explicitation list -> manual_explicitation list
+
+val merge_impls : implicits_list -> implicits_list -> implicits_list
+
+type implicit_interactive_request =
+ | ImplAuto
+ | ImplManual of implicit_status list
+
+type implicit_discharge_request =
+ | ImplLocal
+ | ImplConstant of constant * implicits_flags
+ | ImplMutualInductive of kernel_name * implicits_flags
+ | ImplInteractive of global_reference * implicits_flags *
+ implicit_interactive_request
+
+val discharge_implicits : 'a *
+ (implicit_discharge_request *
+ (Libnames.global_reference *
+ (Names.identifier * implicit_explanation * bool) option list)
+ list) ->
+ (implicit_discharge_request *
+ (Libnames.global_reference *
+ (Names.identifier * implicit_explanation * bool) option list)
+ list)
+ option
+
diff --git a/library/lib.ml b/library/lib.ml
index 4743290ae..31b94cc96 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -216,9 +216,9 @@ let add_leaf id obj =
add_entry oname (Leaf obj);
oname
-let add_discharged_leaf id varinfo obj =
+let add_discharged_leaf id obj =
let oname = make_oname id in
- let newobj = rebuild_object (varinfo, obj) in
+ let newobj = rebuild_object obj in
cache_object (oname,newobj);
add_entry oname (Leaf newobj)
@@ -439,10 +439,12 @@ let what_is_opened () = find_entry_p is_something_opened
- the list of substitution to do at section closing
*)
-type abstr_list = Sign.named_context Names.Cmap.t * Sign.named_context Names.KNmap.t
+type variable_info = Names.identifier * Rawterm.binding_kind * Term.constr option * Term.types
+type variable_context = variable_info list
+type abstr_list = variable_context Names.Cmap.t * variable_context Names.KNmap.t
let sectab =
- ref ([] : ((Names.identifier * bool * Term.types option) list * Cooking.work_list * abstr_list) list)
+ ref ([] : ((Names.identifier * Rawterm.binding_kind * Term.types option) list * Cooking.work_list * abstr_list) list)
let add_section () =
sectab := ([],(Names.Cmap.empty,Names.KNmap.empty),(Names.Cmap.empty,Names.KNmap.empty)) :: !sectab
@@ -453,25 +455,34 @@ let add_section_variable id impl keep =
| (vars,repl,abs)::sl -> sectab := ((id,impl,keep)::vars,repl,abs)::sl
let rec extract_hyps = function
- | ((id,impl,keep)::idl,(id',_,_ as d)::hyps) when id=id' -> d :: extract_hyps (idl,hyps)
- | ((id,impl,Some ty)::idl,hyps) -> (id,None,ty) :: extract_hyps (idl,hyps)
+ | ((id,impl,keep)::idl,(id',b,t)::hyps) when id=id' -> (id',impl,b,t) :: extract_hyps (idl,hyps)
+ | ((id,impl,Some ty)::idl,hyps) -> (id,impl,None,ty) :: extract_hyps (idl,hyps)
| (id::idl,hyps) -> extract_hyps (idl,hyps)
| [], _ -> []
+let instance_from_variable_context sign =
+ let rec inst_rec = function
+ | (id,b,None,_) :: sign -> id :: inst_rec sign
+ | _ :: sign -> inst_rec sign
+ | [] -> [] in
+ Array.of_list (inst_rec sign)
+
+let named_of_variable_context = List.map (fun (id,_,b,t) -> (id,b,t))
+
let add_section_replacement f g hyps =
match !sectab with
| [] -> ()
| (vars,exps,abs)::sl ->
let sechyps = extract_hyps (vars,hyps) in
- let args = Sign.instance_from_named_context (List.rev sechyps) in
- sectab := (vars,f (Array.map Term.destVar args) exps,g sechyps abs)::sl
+ let args = instance_from_variable_context (List.rev sechyps) in
+ sectab := (vars,f args exps,g sechyps abs)::sl
let add_section_kn kn =
- let f = (fun x (l1,l2) -> (l1,Names.KNmap.add kn x l2)) in
+ let f x (l1,l2) = (l1,Names.KNmap.add kn x l2) in
add_section_replacement f f
let add_section_constant kn =
- let f = (fun x (l1,l2) -> (Names.Cmap.add kn x l1,l2)) in
+ let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in
add_section_replacement f f
let replacement_context () = pi2 (List.hd !sectab)
@@ -562,10 +573,6 @@ let close_section id =
with Not_found ->
error "no opened section"
in
- let var_info = List.map
- (fun (x, y, z) -> (x, y, match z with Some _ -> true | None -> false))
- (variables_context ())
- in
let (secdecls,secopening,before) = split_lib oname in
lib_stk := before;
let full_olddir = fst !path_prefix in
@@ -574,7 +581,7 @@ let close_section id =
if !Flags.xml_export then !xml_close_section id;
let newdecls = List.map discharge_item secdecls in
Summary.section_unfreeze_summaries fs;
- List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id var_info o)) newdecls;
+ List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls;
Cooking.clear_cooking_sharing ();
Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir)
diff --git a/library/lib.mli b/library/lib.mli
index c13f7f62d..42a68f0ed 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -168,14 +168,19 @@ val set_xml_close_section : (Names.identifier -> unit) -> unit
(*s Section management for discharge *)
+type variable_info = Names.identifier * Rawterm.binding_kind * Term.constr option * Term.types
+type variable_context = variable_info list
-val section_segment_of_constant : Names.constant -> Sign.named_context
-val section_segment_of_mutual_inductive: Names.mutual_inductive -> Sign.named_context
+val instance_from_variable_context : variable_context -> Names.identifier array
+val named_of_variable_context : variable_context -> Sign.named_context
+
+val section_segment_of_constant : Names.constant -> variable_context
+val section_segment_of_mutual_inductive: Names.mutual_inductive -> variable_context
val section_instance : Libnames.global_reference -> Names.identifier array
val is_in_section : Libnames.global_reference -> bool
-val add_section_variable : Names.identifier -> bool -> Term.types option -> unit
+val add_section_variable : Names.identifier -> Rawterm.binding_kind -> Term.types option -> unit
val add_section_constant : Names.constant -> Sign.named_context -> unit
val add_section_kn : Names.kernel_name -> Sign.named_context -> unit
val replacement_context : unit ->
diff --git a/library/libobject.ml b/library/libobject.ml
index b24a46e38..684607b4b 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -28,8 +28,6 @@ let relax b = relax_flag := b;;
type 'a substitutivity =
Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
-type discharge_info = (identifier * bool * bool) list
-
type 'a object_declaration = {
object_name : string;
cache_function : object_name * 'a -> unit;
@@ -38,7 +36,7 @@ type 'a object_declaration = {
classify_function : object_name * 'a -> 'a substitutivity;
subst_function : object_name * substitution * 'a -> 'a;
discharge_function : object_name * 'a -> 'a option;
- rebuild_function : discharge_info * 'a -> 'a;
+ rebuild_function : 'a -> 'a;
export_function : 'a -> 'a option }
let yell s = anomaly s
@@ -52,7 +50,7 @@ let default_object s = {
yell ("The object "^s^" does not know how to substitute!"));
classify_function = (fun (_,obj) -> Keep obj);
discharge_function = (fun _ -> None);
- rebuild_function = (fun (_,x) -> x);
+ rebuild_function = (fun x -> x);
export_function = (fun _ -> None)}
@@ -78,7 +76,7 @@ type dynamic_object_declaration = {
dyn_subst_function : object_name * substitution * obj -> obj;
dyn_classify_function : object_name * obj -> obj substitutivity;
dyn_discharge_function : object_name * obj -> obj option;
- dyn_rebuild_function : discharge_info * obj -> obj;
+ dyn_rebuild_function : obj -> obj;
dyn_export_function : obj -> obj option }
let object_tag lobj = Dyn.tag lobj
@@ -116,8 +114,8 @@ let declare_object odecl =
Option.map infun (odecl.discharge_function (oname,outfun lobj))
else
anomaly "somehow we got the wrong dynamic object in the dischargefun"
- and rebuild (varinfo,lobj) =
- if Dyn.tag lobj = na then infun (odecl.rebuild_function (varinfo,outfun lobj))
+ and rebuild lobj =
+ if Dyn.tag lobj = na then infun (odecl.rebuild_function (outfun lobj))
else anomaly "somehow we got the wrong dynamic object in the rebuildfun"
and exporter lobj =
if Dyn.tag lobj = na then
@@ -174,7 +172,7 @@ let classify_object ((_,lobj) as node) =
let discharge_object ((_,lobj) as node) =
apply_dyn_fun None (fun d -> d.dyn_discharge_function node) lobj
-let rebuild_object ((_,lobj) as node) =
+let rebuild_object (lobj as node) =
apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function node) lobj
let export_object lobj =
diff --git a/library/libobject.mli b/library/libobject.mli
index 33ad67c84..61e650e6b 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -71,8 +71,6 @@ open Mod_subst
type 'a substitutivity =
Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
-type discharge_info = (identifier * bool * bool) list
-
type 'a object_declaration = {
object_name : string;
cache_function : object_name * 'a -> unit;
@@ -81,7 +79,7 @@ type 'a object_declaration = {
classify_function : object_name * 'a -> 'a substitutivity;
subst_function : object_name * substitution * 'a -> 'a;
discharge_function : object_name * 'a -> 'a option;
- rebuild_function : discharge_info * 'a -> 'a;
+ rebuild_function : 'a -> 'a;
export_function : 'a -> 'a option }
(* The default object is a "Keep" object with empty methods.
@@ -116,5 +114,5 @@ val subst_object : object_name * substitution * obj -> obj
val classify_object : object_name * obj -> obj substitutivity
val export_object : obj -> obj option
val discharge_object : object_name * obj -> obj option
-val rebuild_object : discharge_info * obj -> obj
+val rebuild_object : obj -> obj
val relax : bool -> unit
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index da30b2057..d54eaf00e 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -197,8 +197,8 @@ let discharge (_,(cl,m,inst)) =
let ctx = abs_context cl in
{ cl with cl_impl = cl_impl';
cl_context =
- List.map (fun (na,b,t) -> None, (Name na,b,t)) ctx @
- (discharge_context (List.map pi1 ctx) cl.cl_context);
+ List.map (fun (na,impl,b,t) -> None, (Name na,b,t)) ctx @
+ (discharge_context (List.map (fun (na, _, _, _) -> na) ctx) cl.cl_context);
cl_projs = list_smartmap (fun (x, y) -> x, Lib.discharge_con y) cl.cl_projs }
in Gmap.add cl_impl' cl' acc
in
@@ -216,7 +216,7 @@ let discharge (_,(cl,m,inst)) =
let instances = Gmap.fold subst_inst inst Gmap.empty in
Some (classes, m, instances)
-let rebuild (_,(cl,m,inst)) =
+let rebuild (cl,m,inst) =
let inst =
Gmap.map (fun insts ->
Cmap.fold (fun k is insts ->
diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v
index e7795733f..84ec298df 100644
--- a/test-suite/success/ImplicitArguments.v
+++ b/test-suite/success/ImplicitArguments.v
@@ -2,6 +2,8 @@ Inductive vector {A : Type} : nat -> Type :=
| vnil : vector 0
| vcons : A -> forall {n'}, vector n' -> vector (S n').
+Implicit Arguments vector [].
+
Require Import Coq.Program.Program.
Program Definition head {A : Type} {n : nat} (v : vector A (S n)) : vector A n :=
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index e4df5acbf..9f3b3343c 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -492,10 +492,12 @@ let context ?(hook=fun _ -> ()) l =
add_instance (Typeclasses.new_instance tc None false cst);
hook (ConstRef cst)
| None -> ()
- else
- (Command.declare_one_assumption false (Local (* global *), Definitional) t
- [] true (* implicit *) true (* always kept *) false (* inline *) (dummy_loc, id);
- match class_of_constr t with
- None -> ()
- | Some tc -> hook (VarRef id)))
+ else (
+ let impl = List.exists (fun (x,_) -> match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls
+ in
+ Command.declare_one_assumption false (Local (* global *), Definitional) t
+ [] impl (* implicit *) true (* always kept *) false (* inline *) (dummy_loc, id);
+ match class_of_constr t with
+ | None -> ()
+ | Some tc -> hook (VarRef id)))
(List.rev ctx)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 65b36edb6..afa667ad9 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -785,6 +785,14 @@ let _ =
let _ =
declare_bool_option
{ optsync = true;
+ optname = "manual implicit arguments";
+ optkey = (TertiaryTable ("Manual","Implicit","Arguments"));
+ optread = Impargs.is_manual_implicit_args;
+ optwrite = Impargs.make_manual_implicit_args }
+
+let _ =
+ declare_bool_option
+ { optsync = true;
optname = "strict implicit arguments";
optkey = (SecondaryTable ("Strict","Implicit"));
optread = Impargs.is_strict_implicit_args;
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 10:59:58 +0000