aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/extraction/extract_env.ml1
-rw-r--r--contrib/extraction/haskell.mli2
-rw-r--r--contrib/romega/const_omega.ml15
-rw-r--r--contrib/xml/xmlcommand.ml13
-rw-r--r--kernel/names.ml9
-rw-r--r--kernel/names.mli10
-rw-r--r--kernel/term.ml9
-rw-r--r--kernel/term.mli9
-rwxr-xr-xlibrary/nametab.ml3
-rwxr-xr-xlibrary/nametab.mli1
-rw-r--r--parsing/coqlib.mli1
-rwxr-xr-xtoplevel/recordobj.mli2
12 files changed, 36 insertions, 39 deletions
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 93e8d4cf50..68ff965b25 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -10,6 +10,7 @@
open Pp
open Util
+open Names
open Term
open Lib
open Extraction
diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli
index 77bea2b8b5..4f380271f5 100644
--- a/contrib/extraction/haskell.mli
+++ b/contrib/extraction/haskell.mli
@@ -12,7 +12,7 @@
open Miniml
open Mlutil
-open Term
+open Names
val extract_to_file :
string -> extraction_params -> ml_decl list -> global_reference list -> unit
diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml
index 173c443566..c358e593d6 100644
--- a/contrib/romega/const_omega.ml
+++ b/contrib/romega/const_omega.ml
@@ -20,14 +20,15 @@ let destructurate t =
match Term.kind_of_term c, args with
| Term.IsConst sp, args ->
Kapp (Names.string_of_id
- (Names.basename (Global.sp_of_global (Term.ConstRef sp))),args)
+ (Names.basename (Global.sp_of_global (Names.ConstRef sp))),
+ args)
| Term.IsMutConstruct csp , args ->
Kapp (Names.string_of_id
- (Names.basename (Global.sp_of_global (Term.ConstructRef csp))),
- args)
+ (Names.basename (Global.sp_of_global(Names.ConstructRef csp))),
+ args)
| Term.IsMutInd isp, args ->
Kapp (Names.string_of_id
- (Names.basename (Global.sp_of_global (Term.IndRef isp))),args)
+ (Names.basename (Global.sp_of_global (Names.IndRef isp))),args)
| Term.IsVar id,[] -> Kvar(Names.string_of_id id)
| Term.IsProd (Names.Anonymous,typ,body), [] -> Kimp(typ,body)
| Term.IsProd (Names.Name _,_,_),[] ->
@@ -40,9 +41,9 @@ let dest_const_apply t =
let f,args = Reduction.whd_stack t in
let ref =
match Term.kind_of_term f with
- | Term.IsConst sp -> Term.ConstRef sp
- | Term.IsMutConstruct csp -> Term.ConstructRef csp
- | Term.IsMutInd isp -> Term.IndRef isp
+ | Term.IsConst sp -> Names.ConstRef sp
+ | Term.IsMutConstruct csp -> Names.ConstructRef csp
+ | Term.IsMutInd isp -> Names.IndRef isp
| _ -> raise Destruct
in
Names.basename (Global.sp_of_global ref), args
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index d79e43813d..903a8c0ed4 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -702,20 +702,21 @@ let pp_cmds_of_inner_types inner_types target_uri =
let print sp fn =
let module D = Declarations in
let module G = Global in
- let module N = Nametab in
+ let module N = Names in
+ let module Nt = Nametab in
let module T = Term in
let module X = Xml in
- let (_,id) = N.repr_qualid sp in
+ let (_,id) = Nt.repr_qualid sp in
let glob_ref = Nametab.locate sp in
let env = (Safe_typing.env_of_safe_env (G.safe_env ())) in
reset_ids () ;
let inner_types = ref [] in
let sp,tag,pp_cmds =
match glob_ref with
- T.VarRef sp ->
+ N.VarRef sp ->
let (body,typ) = G.lookup_named id in
sp,Variable,print_variable id body (T.body_of_type typ) env inner_types
- | T.ConstRef sp ->
+ | N.ConstRef sp ->
let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
G.lookup_constant sp in
let hyps = string_list_of_named_context_list hyps in
@@ -726,12 +727,12 @@ let print sp fn =
None -> print_axiom id typ [] hyps env inner_types
| Some c -> print_definition id c typ [] hyps env inner_types
end
- | T.IndRef (sp,_) ->
+ | N.IndRef (sp,_) ->
let {D.mind_packets=packs ; D.mind_hyps=hyps} = G.lookup_mind sp in
let hyps = string_list_of_named_context_list hyps in
sp,Inductive,
print_mutual_inductive packs [] hyps env inner_types
- | T.ConstructRef _ ->
+ | N.ConstructRef _ ->
Util.anomaly ("print: this should not happen")
in
Xml.pp pp_cmds fn ;
diff --git a/kernel/names.ml b/kernel/names.ml
index 811672ba3d..3aa20400a1 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -314,7 +314,8 @@ module Spset = Set.Make(SpOrdered)
module Sppred = Predicate.Make(SpOrdered)
module Spmap = Map.Make(SpOrdered)
-(* Special references for inductive objects *)
+(*s********************************************************************)
+(* type of global reference *)
type variable = section_path
type constant = section_path
@@ -322,6 +323,12 @@ type inductive = section_path * int
type constructor = inductive * int
type mutual_inductive = section_path
+type global_reference =
+ | VarRef of section_path
+ | ConstRef of constant
+ | IndRef of inductive
+ | ConstructRef of constructor
+
(* Hash-consing of name objects *)
module Hname = Hashcons.Make(
struct
diff --git a/kernel/names.mli b/kernel/names.mli
index cdf8c8c83a..a50dc28c4d 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -111,13 +111,21 @@ module Spset : Set.S with type elt = section_path
module Sppred : Predicate.S with type elt = section_path
module Spmap : Map.S with type key = section_path
-(*s Specific paths for declarations *)
+(*s********************************************************************)
+(* type of global reference *)
+
type variable = section_path
type constant = section_path
type inductive = section_path * int
type constructor = inductive * int
type mutual_inductive = section_path
+type global_reference =
+ | VarRef of section_path
+ | ConstRef of constant
+ | IndRef of inductive
+ | ConstructRef of constructor
+
(* Hash-consing *)
val hcons_names : unit ->
(section_path -> section_path) * (section_path -> section_path) *
diff --git a/kernel/term.ml b/kernel/term.ml
index e79fd5fb36..ea720dbd38 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -58,15 +58,6 @@ let family_of_sort = function
| Type _ -> InType
(********************************************************************)
-(* type of global reference *)
-
-type global_reference =
- | VarRef of section_path
- | ConstRef of constant
- | IndRef of inductive
- | ConstructRef of constructor
-
-(********************************************************************)
(* Constructions as implemented *)
(********************************************************************)
diff --git a/kernel/term.mli b/kernel/term.mli
index 248d572276..418ce22368 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -64,15 +64,6 @@ type ('constr, 'types) cofixpoint =
end
(*s*******************************************************************)
-(* type of global reference *)
-
-type global_reference =
- | VarRef of section_path
- | ConstRef of constant
- | IndRef of inductive
- | ConstructRef of constructor
-
-(*s*******************************************************************)
(* The type of constructions *)
type constr
diff --git a/library/nametab.ml b/library/nametab.ml
index 643c4ff165..f09787866d 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -11,9 +11,6 @@
open Util
open Pp
open Names
-open Libobject
-open Declarations
-open Term
(*s qualified names *)
type qualid = dir_path * identifier
diff --git a/library/nametab.mli b/library/nametab.mli
index 5150c18b14..44e4e6b44d 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -12,7 +12,6 @@
open Util
open Pp
open Names
-open Term
(*i*)
(*s This module contains the table for globalization, which associates global
diff --git a/parsing/coqlib.mli b/parsing/coqlib.mli
index 92292161af..1ee79d8868 100644
--- a/parsing/coqlib.mli
+++ b/parsing/coqlib.mli
@@ -9,6 +9,7 @@
(* $Id$ *)
(*i*)
+open Names
open Term
open Pattern
(*i*)
diff --git a/toplevel/recordobj.mli b/toplevel/recordobj.mli
index dec66afe7e..90eadf4046 100755
--- a/toplevel/recordobj.mli
+++ b/toplevel/recordobj.mli
@@ -8,6 +8,6 @@
(* $Id$ *)
-open Term
+open Names
val objdef_declare : global_reference -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:22:41 +0000