From 2debc4ab0b171963afff40cc3183e4e92cca9a0e Mon Sep 17 00:00:00 2001 From: msozeau Date: Tue, 22 Jul 2008 14:02:22 +0000 Subject: Correct implementation of discharging of implicit arguments and add new setting "Set Manual Implicit Arguments" for manual-only implicits. Fix test-suite script. This removes the discharge_info argument of "dynamic" object's rebuild function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11242 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/notation.ml | 2 +- library/declare.ml | 12 +++-- library/heads.ml | 2 +- library/impargs.ml | 96 +++++++++++++++++++++++++--------- library/impargs.mli | 43 +++++++++++++-- library/lib.ml | 37 +++++++------ library/lib.mli | 11 ++-- library/libobject.ml | 14 +++-- library/libobject.mli | 6 +-- pretyping/typeclasses.ml | 6 +-- test-suite/success/ImplicitArguments.v | 2 + toplevel/classes.ml | 14 ++--- toplevel/vernacentries.ml | 8 +++ 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 @@ -782,6 +782,14 @@ let _ = optread = Impargs.is_implicit_args; optwrite = Impargs.make_implicit_args } +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; -- cgit v1.2.3