diff options
| -rw-r--r-- | library/declare.ml | 4 | ||||
| -rw-r--r-- | library/impargs.ml | 4 | ||||
| -rw-r--r-- | library/lib.ml | 5 | ||||
| -rw-r--r-- | library/lib.mli | 5 | ||||
| -rw-r--r-- | pretyping/rawterm.ml | 2 | ||||
| -rw-r--r-- | pretyping/rawterm.mli | 2 |
6 files changed, 12 insertions, 10 deletions
diff --git a/library/declare.ml b/library/declare.ml index e250ec282..0fc9772da 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -57,12 +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 - let impl = if impl then Rawterm.Implicit else Rawterm.Explicit in + let impl = if impl then Lib.Implicit else Lib.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 - Rawterm.Explicit, opaq, cst, None in + Lib.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 []; diff --git a/library/impargs.ml b/library/impargs.ml index 4759ced46..bb11ce2f8 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -20,8 +20,8 @@ open Libobject open Lib open Nametab open Pp -open Termops open Topconstr +open Termops (*s Flags governing the computation of implicit arguments *) @@ -468,7 +468,7 @@ 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.rev_map (fun (id,impl,_,_) -> if impl = Lib.Implicit then Some (id, Manual, true) else None) (List.filter (fun (_,_,b,_) -> b = None) ctx) let section_segment_of_reference = function diff --git a/library/lib.ml b/library/lib.ml index 31b94cc96..553d353d6 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -438,13 +438,14 @@ let what_is_opened () = find_entry_p is_something_opened - the list of variables on which each inductive depends in this section - the list of substitution to do at section closing *) +type binding_kind = Explicit | Implicit -type variable_info = Names.identifier * Rawterm.binding_kind * Term.constr option * Term.types +type variable_info = Names.identifier * 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 * Rawterm.binding_kind * Term.types option) list * Cooking.work_list * abstr_list) list) + ref ([] : ((Names.identifier * 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 diff --git a/library/lib.mli b/library/lib.mli index 42a68f0ed..3e64a5290 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -166,9 +166,10 @@ val reset_initial : unit -> unit val set_xml_open_section : (Names.identifier -> unit) -> unit val set_xml_close_section : (Names.identifier -> unit) -> unit +type binding_kind = Explicit | Implicit (*s Section management for discharge *) -type variable_info = Names.identifier * Rawterm.binding_kind * Term.constr option * Term.types +type variable_info = Names.identifier * binding_kind * Term.constr option * Term.types type variable_context = variable_info list val instance_from_variable_context : variable_context -> Names.identifier array @@ -180,7 +181,7 @@ val section_segment_of_mutual_inductive: Names.mutual_inductive -> variable_cont val section_instance : Libnames.global_reference -> Names.identifier array val is_in_section : Libnames.global_reference -> bool -val add_section_variable : Names.identifier -> Rawterm.binding_kind -> Term.types option -> unit +val add_section_variable : Names.identifier -> 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/pretyping/rawterm.ml b/pretyping/rawterm.ml index 79708e9fb..ea622de7f 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -36,7 +36,7 @@ type rawsort = RProp of Term.contents | RType of Univ.universe option type binder_kind = BProd | BLambda | BLetIn -type binding_kind = Explicit | Implicit +type binding_kind = Lib.binding_kind = Explicit | Implicit type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 0eee3e73a..3628e2a50 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -40,7 +40,7 @@ type rawsort = RProp of Term.contents | RType of Univ.universe option type binder_kind = BProd | BLambda | BLetIn -type binding_kind = Explicit | Implicit +type binding_kind = Lib.binding_kind = Explicit | Implicit type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier |