diff options
-rw-r--r-- | contrib/subtac/subtac.ml | 2 | ||||
-rw-r--r-- | interp/notation.ml | 2 | ||||
-rw-r--r-- | library/declare.ml | 12 | ||||
-rw-r--r-- | library/declare.mli | 2 | ||||
-rw-r--r-- | library/impargs.ml | 76 | ||||
-rw-r--r-- | library/impargs.mli | 3 | ||||
-rw-r--r-- | library/lib.ml | 21 | ||||
-rw-r--r-- | library/lib.mli | 2 | ||||
-rw-r--r-- | library/libobject.ml | 15 | ||||
-rw-r--r-- | library/libobject.mli | 6 | ||||
-rw-r--r-- | pretyping/typeclasses.ml | 27 | ||||
-rw-r--r-- | pretyping/typeclasses.mli | 7 | ||||
-rw-r--r-- | toplevel/classes.ml | 7 | ||||
-rw-r--r-- | toplevel/command.ml | 8 | ||||
-rw-r--r-- | toplevel/command.mli | 9 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 2 |
16 files changed, 113 insertions, 88 deletions
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index e7a727bb5..ac4b9642e 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -100,7 +100,7 @@ let declare_assumption env isevars idl is_coe k bl c nl = Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr c bl) None in let c = solve_tccs_in_type env id isevars evm c typ in - List.iter (Command.declare_one_assumption is_coe k c imps nl) idl + List.iter (Command.declare_one_assumption is_coe k c imps false false nl) idl else errorlabstrm "Command.Assumption" (str "Cannot declare an assumption while in proof editing mode.") diff --git a/interp/notation.ml b/interp/notation.ml index b04f3be03..f3ecbd446 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -467,7 +467,7 @@ let discharge_arguments_scope (_,(req,r,l)) = if req = ArgsScopeNoDischarge then None else Some (req,pop_global_reference 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 da2c1b778..278acc665 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -57,7 +57,7 @@ let set_xml_declare_inductive f = xml_declare_inductive := if_xml f type section_variable_entry = | SectionLocalDef of constr * types option * bool (* opacity *) - | SectionLocalAssum of types + | SectionLocalAssum of types * bool * bool (* Implicit status, Keep *) type variable_declaration = dir_path * section_variable_entry * logical_kind @@ -84,17 +84,17 @@ let cache_variable ((sp,_),o) = (* Constr raisonne sur les noms courts *) if Idmap.mem id !vartab then errorlabstrm "cache_variable" (pr_id id ++ str " already exists"); - let vd = match d with (* Fails if not well-typed *) - | SectionLocalAssum ty -> + let vd,impl,keep = match d with (* Fails if not well-typed *) + | SectionLocalAssum (ty, impl, keep) -> let cst = Global.push_named_assum (id,ty) in let (_,bd,ty) = Global.lookup_named id in - CheckedSectionLocalAssum (ty,cst) + CheckedSectionLocalAssum (ty,cst), impl, if keep then Some ty else None | SectionLocalDef (c,t,opaq) -> let cst = Global.push_named_def (id,c,t) in let (_,bd,ty) = Global.lookup_named id in - CheckedSectionLocalDef (Option.get bd,ty,cst,opaq) in + CheckedSectionLocalDef (Option.get bd,ty,cst,opaq), false, None in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); - add_section_variable id; + add_section_variable id impl keep; Dischargedhypsmap.set_discharged_hyps sp []; vartab := Idmap.add id (p,vd,mk) !vartab diff --git a/library/declare.mli b/library/declare.mli index f04170b34..96fd5eb9b 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -34,7 +34,7 @@ open Nametab type section_variable_entry = | SectionLocalDef of constr * types option * bool (* opacity *) - | SectionLocalAssum of types + | SectionLocalAssum of types * bool * bool (* Implicit status, Keep *) type variable_declaration = dir_path * section_variable_entry * logical_kind diff --git a/library/impargs.ml b/library/impargs.ml index 9ffd103de..fc2d63ca8 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -240,12 +240,6 @@ let compute_implicits_flags env f all t = (f.strict or f.strongly_strict) f.strongly_strict f.reversible_pattern f.contextual all env t -let compute_implicits_auto env f t = - let l = compute_implicits_flags env f false t in - prepare_implicits f l - -let compute_implicits env t = compute_implicits_auto env !implicit_args t - let set_implicit id imp insmax = (id,(match imp with None -> Manual false | Some imp -> imp),insmax) @@ -258,7 +252,7 @@ let rec assoc_by_pos k = function | hd :: tl -> let (x, tl) = assoc_by_pos k tl in x, hd :: tl | [] -> raise Not_found -let compute_manual_implicits flags env t enriching l = +let compute_manual_implicits env flags t enriching l = let autoimps = if enriching then compute_implicits_flags env flags true t else compute_implicits_gen false false false true true env t in @@ -296,8 +290,9 @@ let compute_manual_implicits flags env t enriching l = forced :: merge (k+1) l' imps | [] when l = [] -> [] | [] -> - match List.hd l with - | ExplByName id,b -> + List.iter (function + | ExplByName id,(b,forced) -> + if not forced then error ("Wrong or not dependent implicit argument name: "^(string_of_id id)) | ExplByPos (i,_id),_t -> if i<1 or i>n then @@ -305,10 +300,19 @@ let compute_manual_implicits flags env t enriching l = else errorlabstrm "" (str "Cannot set implicit argument number " ++ int i ++ - str ": it has no name") + str ": it has no name")) + l; [] in merge 1 l autoimps +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 compute_implicits env t = compute_implicits_auto env !implicit_args [] t + type maximal_insertion = bool (* true = maximal contextual insertion *) type implicit_status = @@ -353,16 +357,16 @@ let positions_of_implicits = (*s Constants. *) -let compute_constant_implicits flags cst = +let compute_constant_implicits flags manual cst = let env = Global.env () in - compute_implicits_auto env flags (Typeops.type_of_constant env cst) + compute_implicits_auto env flags manual (Typeops.type_of_constant env cst) (*s Inductives and constructors. Their implicit arguments are stored in an array, indexed by the inductive number, of pairs $(i,v)$ where $i$ are the implicit arguments of the inductive and $v$ the array of implicit arguments of the constructors. *) -let compute_mib_implicits flags kn = +let compute_mib_implicits flags manual kn = let env = Global.env () in let mib = lookup_mind kn env in let ar = @@ -375,34 +379,34 @@ let compute_mib_implicits flags kn = let imps_one_inductive i mip = let ind = (kn,i) in let ar = type_of_inductive env (mib,mip) in - ((IndRef ind,compute_implicits_auto env flags ar), + ((IndRef ind,compute_implicits_auto env flags manual ar), Array.mapi (fun j c -> - (ConstructRef (ind,j+1),compute_implicits_auto env_ar flags c)) + (ConstructRef (ind,j+1),compute_implicits_auto env_ar flags manual c)) mip.mind_nf_lc) in Array.mapi imps_one_inductive mib.mind_packets -let compute_all_mib_implicits flags kn = - let imps = compute_mib_implicits flags kn in +let compute_all_mib_implicits flags manual kn = + let imps = compute_mib_implicits flags manual kn in List.flatten (array_map_to_list (fun (ind,cstrs) -> ind::Array.to_list cstrs) imps) (*s Variables. *) -let compute_var_implicits flags id = +let compute_var_implicits flags manual id = let env = Global.env () in let (_,_,ty) = lookup_named id env in - compute_implicits_auto env flags ty + compute_implicits_auto env flags manual ty (* Implicits of a global reference. *) -let compute_global_implicits flags = function - | VarRef id -> compute_var_implicits flags id - | ConstRef kn -> compute_constant_implicits flags kn +let compute_global_implicits flags manual = function + | VarRef id -> compute_var_implicits flags manual id + | ConstRef kn -> compute_constant_implicits flags manual kn | IndRef (kn,i) -> - let ((_,imps),_) = (compute_mib_implicits flags kn).(i) in imps + let ((_,imps),_) = (compute_mib_implicits flags manual kn).(i) in imps | ConstructRef ((kn,i),j) -> - let (_,cimps) = (compute_mib_implicits flags kn).(i) in snd cimps.(j-1) + let (_,cimps) = (compute_mib_implicits flags manual kn).(i) in snd cimps.(j-1) (* Merge a manual explicitation with an implicit_status list *) @@ -459,19 +463,23 @@ let discharge_implicits (_,(req,l)) = | ImplMutualInductive (kn,flags) -> Some (ImplMutualInductive (pop_kn kn,flags),l) -let rebuild_implicits (req,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 l' = match req with | ImplNoDischarge -> assert false | ImplConstant (con,flags) -> - [ConstRef con,compute_constant_implicits flags con] + [ConstRef con, compute_constant_implicits flags manual con] | ImplMutualInductive (kn,flags) -> - compute_all_mib_implicits flags kn + compute_all_mib_implicits flags manual kn | ImplInteractive (ref,flags,o) -> match o with - | ImplAuto -> [ref,compute_global_implicits flags ref] + | ImplAuto -> [ref,compute_global_implicits flags manual ref] | ImplManual l -> - let auto = compute_global_implicits flags ref in - let auto = if flags.main then auto else List.map (fun _ -> None) auto in + 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'] in (req,l') @@ -487,7 +495,7 @@ let (inImplicits, _) = export_function = (fun x -> Some x) } let declare_implicits_gen req flags ref = - let imps = compute_global_implicits flags ref in + let imps = compute_global_implicits flags [] ref in add_anonymous_leaf (inImplicits (req,[ref,imps])) let declare_implicits local ref = @@ -510,7 +518,7 @@ let declare_mib_implicits kn = let flags = !implicit_args in let imps = array_map_to_list (fun (ind,cstrs) -> ind::(Array.to_list cstrs)) - (compute_mib_implicits flags kn) in + (compute_mib_implicits flags [] kn) in add_anonymous_leaf (inImplicits (ImplMutualInductive (kn,flags),List.flatten imps)) @@ -518,13 +526,13 @@ let declare_mib_implicits kn = type manual_explicitation = Topconstr.explicitation * (bool * bool) let compute_implicits_with_manual env typ enriching l = - compute_manual_implicits !implicit_args env typ enriching l + compute_manual_implicits env !implicit_args typ 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 l' = compute_manual_implicits flags env t enriching l in + let l' = compute_manual_implicits env flags t enriching l in let req = if local or isVarRef ref then ImplNoDischarge else ImplInteractive(ref,flags,ImplManual l') diff --git a/library/impargs.mli b/library/impargs.mli index e7b05f422..120660027 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -59,7 +59,8 @@ val compute_implicits : env -> types -> implicits_list maximal insertion and forcing flags. *) type manual_explicitation = Topconstr.explicitation * (bool * bool) -val compute_implicits_with_manual : env -> types -> bool -> manual_explicitation list -> implicits_list +val compute_implicits_with_manual : env -> types -> bool -> + manual_explicitation list -> implicits_list (*s Computation of implicits (done using the global environment). *) diff --git a/library/lib.ml b/library/lib.ml index 4acdba88c..1db433c19 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -214,9 +214,9 @@ let add_leaf id obj = add_entry oname (Leaf obj); oname -let add_discharged_leaf id obj = +let add_discharged_leaf id varinfo obj = let oname = make_oname id in - let newobj = rebuild_object obj in + let newobj = rebuild_object (varinfo, obj) in cache_object (oname,newobj); add_entry oname (Leaf newobj) @@ -440,18 +440,19 @@ let what_is_opened () = find_entry_p is_something_opened type abstr_list = Sign.named_context Cmap.t * Sign.named_context KNmap.t let sectab = - ref ([] : (identifier list * Cooking.work_list * abstr_list) list) + ref ([] : ((identifier * bool * Term.types option) list * Cooking.work_list * abstr_list) list) let add_section () = sectab := ([],(Cmap.empty,KNmap.empty),(Cmap.empty,KNmap.empty)) :: !sectab -let add_section_variable id = +let add_section_variable id impl keep = match !sectab with | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) - | (vars,repl,abs)::sl -> sectab := (id::vars,repl,abs)::sl + | (vars,repl,abs)::sl -> sectab := ((id,impl,keep)::vars,repl,abs)::sl let rec extract_hyps = function - | (id::idl,(id',_,_ as d)::hyps) when id=id' -> d :: extract_hyps (idl,hyps) + | ((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::idl,hyps) -> extract_hyps (idl,hyps) | [], _ -> [] @@ -473,6 +474,8 @@ let add_section_constant kn = let replacement_context () = pi2 (List.hd !sectab) +let variables_context () = pi1 (List.hd !sectab) + let section_segment_of_constant con = Cmap.find con (fst (pi3 (List.hd !sectab))) @@ -548,6 +551,10 @@ 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 @@ -556,7 +563,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 o)) newdecls; + List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id var_info 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 6c826af63..da8ace048 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -175,7 +175,7 @@ val section_segment_of_mutual_inductive: mutual_inductive -> Sign.named_context val section_instance : global_reference -> identifier array -val add_section_variable : identifier -> unit +val add_section_variable : identifier -> bool -> Term.types option -> unit val add_section_constant : constant -> Sign.named_context -> unit val add_section_kn : kernel_name -> Sign.named_context -> unit val replacement_context : unit -> diff --git a/library/libobject.ml b/library/libobject.ml index 7c74d402b..b24a46e38 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -28,6 +28,7 @@ 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; @@ -37,7 +38,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 : 'a -> 'a; + rebuild_function : discharge_info * 'a -> 'a; export_function : 'a -> 'a option } let yell s = anomaly s @@ -51,7 +52,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)} @@ -77,7 +78,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 : obj -> obj; + dyn_rebuild_function : discharge_info * obj -> obj; dyn_export_function : obj -> obj option } let object_tag lobj = Dyn.tag lobj @@ -115,8 +116,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 lobj = - if Dyn.tag lobj = na then infun (odecl.rebuild_function (outfun lobj)) + and rebuild (varinfo,lobj) = + if Dyn.tag lobj = na then infun (odecl.rebuild_function (varinfo,outfun lobj)) else anomaly "somehow we got the wrong dynamic object in the rebuildfun" and exporter lobj = if Dyn.tag lobj = na then @@ -173,8 +174,8 @@ 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 = - apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function lobj) lobj +let rebuild_object ((_,lobj) as node) = + apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function node) lobj let export_object lobj = apply_dyn_fun None (fun d -> d.dyn_export_function lobj) lobj diff --git a/library/libobject.mli b/library/libobject.mli index 540b69feb..15de388ea 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -63,6 +63,8 @@ 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; @@ -71,7 +73,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 : 'a -> 'a; + rebuild_function : discharge_info * 'a -> 'a; export_function : 'a -> 'a option } (* The default object is a "Keep" object with empty methods. @@ -106,5 +108,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 : obj -> obj +val rebuild_object : discharge_info * obj -> obj val relax : bool -> unit diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 4c944f460..191343a55 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id:$ i*) +(*i $Id$ i*) (*i*) open Names @@ -90,8 +90,8 @@ let gmap_list_merge old upd ne = let oldv = try Gmap.find k old with Not_found -> [] in let v' = List.fold_left (fun acc x -> - if not (List.exists (fun y -> y.is_impl = x.is_impl) v) then - (x :: acc) else acc) + if not (List.exists (fun y -> y.is_impl = x.is_impl) v) then ( + (x :: acc)) else acc) v oldv in Gmap.add k v' acc) ne Gmap.empty @@ -106,17 +106,15 @@ let gmap_list_merge old upd ne = old ne let add_instance_hint_ref = ref (fun id pri -> assert false) -let register_add_instance_hint = (:=) add_instance_hint_ref +let register_add_instance_hint = + (:=) add_instance_hint_ref let add_instance_hint id = !add_instance_hint_ref id -let qualid_of_con c = - Qualid (dummy_loc, shortest_qualid_of_global Idset.empty (ConstRef c)) - let cache (_, (cl, m, inst)) = classes := gmap_merge !classes cl; methods := gmap_merge !methods m; - instances := gmap_list_merge !instances - (fun i -> add_instance_hint (qualid_of_con i.is_impl)) + instances := gmap_list_merge !instances + (fun (i : instance) -> add_instance_hint i.is_impl i.is_pri) inst open Libobject @@ -179,11 +177,17 @@ let discharge (_,(cl,m,inst)) = { is_impl = Lib.discharge_con is.is_impl; is_pri = is.is_pri; is_class = Gmap.find (Lib.discharge_global is.is_class.cl_impl) classes; }) - insts + insts; in let instances = Gmap.map subst_inst inst in Some (classes, m, instances) +let rebuild (_,(cl,m,inst as obj)) = + Gmap.iter (fun _ insts -> + List.iter (fun is -> add_instance_hint is.is_impl is.is_pri) insts) + inst; + obj + let (input,output) = declare_object { (default_object "type classes state") with @@ -192,6 +196,7 @@ let (input,output) = open_function = (fun _ -> cache); classify_function = (fun (_,x) -> Substitute x); discharge_function = discharge; +(* rebuild_function = rebuild; *) subst_function = subst; export_function = (fun x -> Some x) } @@ -228,7 +233,7 @@ let instances_of c = let add_instance i = let cl = Gmap.find i.is_class.cl_impl !classes in instances := gmapl_add cl.cl_impl { i with is_class = cl } !instances; - add_instance_hint (qualid_of_con i.is_impl) i.is_pri; + add_instance_hint i.is_impl i.is_pri; update () let instances r = diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 2646c09dd..c091842f0 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -52,8 +52,8 @@ val typeclasses : unit -> typeclass list val add_class : typeclass -> unit val add_instance : instance -> unit -val register_add_instance_hint : (reference -> int option -> unit) -> unit -val add_instance_hint : reference -> int option -> unit +val register_add_instance_hint : (constant -> int option -> unit) -> unit +val add_instance_hint : constant -> int option -> unit val class_info : global_reference -> typeclass (* raises a UserError if not a class *) val is_class : global_reference -> bool @@ -89,9 +89,6 @@ val nf_substitution : evar_map -> substitution -> substitution val is_implicit_arg : hole_kind -> bool -val qualid_of_con : Names.constant -> Libnames.reference - - (* debug *) (* val subst : *) diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 535dda623..bc627a283 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -33,11 +33,14 @@ open Entries let hint_db = "typeclass_instances" +let qualid_of_con c = + Qualid (dummy_loc, shortest_qualid_of_global Idset.empty (ConstRef c)) + let _ = Typeclasses.register_add_instance_hint (fun inst pri -> Auto.add_hints false [hint_db] - (Vernacexpr.HintsResolve [pri, CAppExpl (dummy_loc, (None, inst), [])])) + (Vernacexpr.HintsResolve [pri, CAppExpl (dummy_loc, (None, qualid_of_con inst), [])])) let declare_instance_constant con = let instance = Typeops.type_of_constant (Global.env ()) con in @@ -593,7 +596,7 @@ let context ?(hook=fun _ -> ()) l = | None -> () else (Command.declare_one_assumption false (Local (* global *), Definitional) t - [] false (* inline *) (dummy_loc, id); + [] true (* implicit *) true (* always kept *) false (* inline *) (dummy_loc, id); match class_of_constr t with None -> () | Some tc -> hook (VarRef id))) diff --git a/toplevel/command.ml b/toplevel/command.ml index fbba7a4ee..bc8f6c9ee 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -172,12 +172,12 @@ let syntax_definition ident (vars,c) local onlyparse = let assumption_message id = if_verbose message ((string_of_id id) ^ " is assumed") -let declare_one_assumption is_coe (local,kind) c imps nl (_,ident) = +let declare_one_assumption is_coe (local,kind) c imps impl keep nl (_,ident) = let r = match local with | Local when Lib.sections_are_opened () -> let _ = declare_variable ident - (Lib.cwd(), SectionLocalAssum c, IsAssumption kind) in + (Lib.cwd(), SectionLocalAssum (c,impl,keep), IsAssumption kind) in assumption_message ident; if is_verbose () & Pfedit.refining () then msgerrnl (str"Warning: Variable " ++ pr_id ident ++ @@ -198,13 +198,13 @@ let declare_one_assumption is_coe (local,kind) c imps nl (_,ident) = let declare_assumption_hook = ref ignore let set_declare_assumption_hook = (:=) declare_assumption_hook -let declare_assumption idl is_coe k bl c nl= +let declare_assumption idl is_coe k bl c impl keep nl = if not (Pfedit.refining ()) then let c = generalize_constr_expr c bl in let env = Global.env () in let c', imps = interp_type_evars_impls env c in !declare_assumption_hook c'; - List.iter (declare_one_assumption is_coe k c' imps nl) idl + List.iter (declare_one_assumption is_coe k c' imps impl keep nl) idl else errorlabstrm "Command.Assumption" (str "Cannot declare an assumption while in proof editing mode.") diff --git a/toplevel/command.mli b/toplevel/command.mli index 942fd2c31..8a987ef6c 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -43,13 +43,14 @@ val syntax_definition : identifier -> identifier list * constr_expr -> bool -> bool -> unit val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types -> - Impargs.manual_explicitation list -> bool -> Names.variable located -> unit - + Impargs.manual_explicitation list -> + bool (* implicit *) -> bool (* keep *) -> bool (* inline *) -> Names.variable located -> unit + val set_declare_assumption_hook : (types -> unit) -> unit val declare_assumption : identifier located list -> - coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> bool - ->unit + coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> + bool -> bool -> bool -> unit val declare_interning_data : 'a * Constrintern.implicits_env -> string * Topconstr.constr_expr * Topconstr.scope_name option -> unit diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 1ea732add..f5768888c 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -353,7 +353,7 @@ let vernac_exact_proof c = (str "Command 'Proof ...' can only be used at the beginning of the proof") let vernac_assumption kind l nl= - List.iter (fun (is_coe,(idl,c)) -> declare_assumption idl is_coe kind [] c nl) l + List.iter (fun (is_coe,(idl,c)) -> declare_assumption idl is_coe kind [] c false false nl) l let vernac_inductive f indl = build_mutual indl f |