diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/declare.ml | 20 | ||||
| -rw-r--r-- | interp/declare.mli | 6 | ||||
| -rw-r--r-- | interp/dumpglob.ml | 2 | ||||
| -rw-r--r-- | interp/dumpglob.mli | 6 | ||||
| -rw-r--r-- | interp/impargs.ml | 4 | ||||
| -rw-r--r-- | interp/impargs.mli | 4 | ||||
| -rw-r--r-- | interp/notation.ml | 2 | ||||
| -rw-r--r-- | interp/notation.mli | 2 | ||||
| -rw-r--r-- | interp/syntax_def.mli | 2 |
9 files changed, 24 insertions, 24 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index bd8f3db50..0ead94eff 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -136,31 +136,31 @@ let check_exists sp = let cache_constant ((sp,kn), obj) = let id = basename sp in - let _,dir,_ = repr_kn kn in + let _,dir,_ = KerName.repr kn in let kn' = match obj.cst_decl with | None -> if Global.exists_objlabel (Label.of_id (basename sp)) - then constant_of_kn kn + then Constant.make1 kn else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".") | Some decl -> let () = check_exists sp in Global.add_constant dir id decl in - assert (eq_constant kn' (constant_of_kn kn)); - Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn)); + assert (Constant.equal kn' (Constant.make1 kn)); + Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn)); let cst = Global.lookup_constant kn' in add_section_constant (Declareops.constant_is_polymorphic cst) kn' cst.const_hyps; Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps; - add_constant_kind (constant_of_kn kn) obj.cst_kind + add_constant_kind (Constant.make1 kn) obj.cst_kind let discharged_hyps kn sechyps = - let (_,dir,_) = repr_kn kn in + let (_,dir,_) = KerName.repr kn in let args = Array.to_list (instance_from_variable_context sechyps) in List.rev_map (Libnames.make_path dir) args let discharge_constant ((sp, kn), obj) = - let con = constant_of_kn kn in + let con = Constant.make1 kn in let from = Global.lookup_constant con in let modlist = replacement_context () in let hyps,subst,uctx = section_segment_of_constant con in @@ -311,9 +311,9 @@ let cache_inductive ((sp,kn),(dhyps,mie)) = let names = inductive_names sp kn mie in List.iter check_exists (List.map fst names); let id = basename sp in - let _,dir,_ = repr_kn kn in + let _,dir,_ = KerName.repr kn in let kn' = Global.add_mind dir id mie in - assert (eq_mind kn' (mind_of_kn kn)); + assert (MutInd.equal kn' (MutInd.make1 kn)); let mind = Global.lookup_mind kn' in add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps; Dischargedhypsmap.set_discharged_hyps sp dhyps; @@ -384,7 +384,7 @@ let declare_projections mind = let kn' = declare_constant id (ProjectionEntry entry, IsDefinition StructureComponent) in - assert(eq_constant kn kn')) kns; true,true + assert(Constant.equal kn kn')) kns; true,true | Some None -> true,false | None -> false,false diff --git a/interp/declare.mli b/interp/declare.mli index ccd7d28bb..86d33cfb2 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -52,17 +52,17 @@ val definition_entry : ?fix_exn:Future.fix_exn -> internal specify if the constant has been created by the kernel or by the user, and in the former case, if its errors should be silent *) val declare_constant : - ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant + ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> Constant.t val declare_definition : ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> - constr Univ.in_universe_context_set -> constant + constr Univ.in_universe_context_set -> Constant.t (** Since transparent constants' side effects are globally declared, we * need that *) val set_declare_scheme : - (string -> (inductive * constant) array -> unit) -> unit + (string -> (inductive * Constant.t) array -> unit) -> unit (** [declare_mind me] declares a block of inductive types with their constructors in the current section; it returns the path of diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 561b0078a..13ed65056 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -231,7 +231,7 @@ let add_glob ?loc ref = add_glob_gen ?loc sp lib_dp ty let mp_of_kn kn = - let mp,sec,l = Names.repr_kn kn in + let mp,sec,l = Names.KerName.repr kn in Names.MPdot (mp,l) let add_glob_kn ?loc kn = diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index afcd7a2ed..f3ad50f28 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -23,11 +23,11 @@ val pause : unit -> unit val continue : unit -> unit val add_glob : ?loc:Loc.t -> Globnames.global_reference -> unit -val add_glob_kn : ?loc:Loc.t -> Names.kernel_name -> unit +val add_glob_kn : ?loc:Loc.t -> Names.KerName.t -> unit val dump_definition : Names.Id.t Loc.located -> bool -> string -> unit -val dump_moddef : ?loc:Loc.t -> Names.module_path -> string -> unit -val dump_modref : ?loc:Loc.t -> Names.module_path -> string -> unit +val dump_moddef : ?loc:Loc.t -> Names.ModPath.t -> string -> unit +val dump_modref : ?loc:Loc.t -> Names.ModPath.t -> string -> unit val dump_reference : ?loc:Loc.t -> string -> string -> string -> unit val dump_libref : ?loc:Loc.t -> Names.DirPath.t -> string -> unit val dump_notation_location : (int * int) list -> Constrexpr.notation -> diff --git a/interp/impargs.ml b/interp/impargs.ml index 09a0ba83c..daec1191e 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -483,8 +483,8 @@ type implicit_interactive_request = type implicit_discharge_request = | ImplLocal - | ImplConstant of constant * implicits_flags - | ImplMutualInductive of mutual_inductive * implicits_flags + | ImplConstant of Constant.t * implicits_flags + | ImplMutualInductive of MutInd.t * implicits_flags | ImplInteractive of global_reference * implicits_flags * implicit_interactive_request diff --git a/interp/impargs.mli b/interp/impargs.mli index 4b78f54ea..658d9e01a 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -98,8 +98,8 @@ val compute_implicits_names : env -> types -> Name.t list (** {6 Computation of implicits (done using the global environment). } *) val declare_var_implicits : variable -> unit -val declare_constant_implicits : constant -> unit -val declare_mib_implicits : mutual_inductive -> unit +val declare_constant_implicits : Constant.t -> unit +val declare_mib_implicits : MutInd.t -> unit val declare_implicits : bool -> global_reference -> unit diff --git a/interp/notation.ml b/interp/notation.ml index d3cac1e3e..076570c8a 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -234,7 +234,7 @@ let find_delimiters_scope ?loc key = type interp_rule = | NotationRule of scope_name option * notation - | SynDefRule of kernel_name + | SynDefRule of KerName.t (* We define keys for glob_constr and aconstr to split the syntax entries according to the key of the pattern (adapted from Chet Murthy by HH) *) diff --git a/interp/notation.mli b/interp/notation.mli index 75c8d5aa5..e312a3767 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -110,7 +110,7 @@ val availability_of_prim_token : (** Binds a notation in a given scope to an interpretation *) type interp_rule = | NotationRule of scope_name option * notation - | SynDefRule of kernel_name + | SynDefRule of KerName.t val declare_notation_interpretation : notation -> scope_name option -> interpretation -> notation_location -> onlyprint:bool -> unit diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index 36a3986b5..4d2cb5b74 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -16,4 +16,4 @@ type syndef_interpretation = (Id.t * subscopes) list * notation_constr val declare_syntactic_definition : bool -> Id.t -> Flags.compat_version option -> syndef_interpretation -> unit -val search_syntactic_definition : kernel_name -> syndef_interpretation +val search_syntactic_definition : KerName.t -> syndef_interpretation |