aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml2
-rw-r--r--interp/constrextern.mli3
-rw-r--r--interp/constrintern.mli2
-rw-r--r--interp/declare.ml6
-rw-r--r--interp/declare.mli6
-rw-r--r--interp/discharge.ml1
-rw-r--r--interp/impargs.ml13
-rw-r--r--interp/impargs.mli2
-rw-r--r--interp/notation.ml4
-rw-r--r--interp/notation.mli4
10 files changed, 22 insertions, 21 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index bd6aa0911..e1cf8f196 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -12,7 +12,7 @@ open CErrors
open Util
open Names
open Nameops
-open Term
+open Constr
open Termops
open Libnames
open Globnames
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index b2df449c5..d980b1995 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Names
-open Term
open Termops
open EConstr
open Environ
@@ -41,7 +40,7 @@ val extern_constr : ?lax:bool -> bool -> env -> Evd.evar_map -> constr -> constr
val extern_constr_in_scope : bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr
val extern_reference : ?loc:Loc.t -> Id.Set.t -> global_reference -> reference
val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
-val extern_sort : Evd.evar_map -> sorts -> glob_sort
+val extern_sort : Evd.evar_map -> Sorts.t -> glob_sort
val extern_rel_context : constr option -> env -> Evd.evar_map ->
rel_context -> local_binder_expr list
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 75e99dd9b..46f96d20b 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -7,7 +7,7 @@
(************************************************************************)
open Names
-open Term
+open Constr
open Evd
open Environ
open Libnames
diff --git a/interp/declare.ml b/interp/declare.ml
index 0ead94eff..0cc4d0fca 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -15,7 +15,7 @@ open Names
open Libnames
open Globnames
open Nameops
-open Term
+open Constr
open Declarations
open Entries
open Libobject
@@ -440,7 +440,7 @@ let assumption_message id =
(** Global universe names, in a different summary *)
-type universe_context_decl = polymorphic * Univ.universe_context_set
+type universe_context_decl = polymorphic * Univ.ContextSet.t
let cache_universe_context (p, ctx) =
Global.push_context_set p ctx;
@@ -458,7 +458,7 @@ let declare_universe_context poly ctx =
Lib.add_anonymous_leaf (input_universe_context (poly, ctx))
(* Discharged or not *)
-type universe_decl = polymorphic * (Id.t * Univ.universe_level) list
+type universe_decl = polymorphic * (Id.t * Univ.Level.t) list
let cache_universes (p, l) =
let glob = Global.global_universe_names () in
diff --git a/interp/declare.mli b/interp/declare.mli
index 86d33cfb2..9b3194dec 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -8,7 +8,7 @@
open Names
open Libnames
-open Term
+open Constr
open Entries
open Decl_kinds
@@ -42,7 +42,7 @@ type internal_flag =
(* Defaut definition entries, transparent with no secctx or proj information *)
val definition_entry : ?fix_exn:Future.fix_exn ->
?opaque:bool -> ?inline:bool -> ?types:types ->
- ?poly:polymorphic -> ?univs:Univ.universe_context ->
+ ?poly:polymorphic -> ?univs:Univ.UContext.t ->
?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry
(** [declare_constant id cd] declares a global declaration
@@ -84,7 +84,7 @@ val exists_name : Id.t -> bool
(** Global universe contexts, names and constraints *)
-val declare_universe_context : polymorphic -> Univ.universe_context_set -> unit
+val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit
val do_universe : polymorphic -> Id.t Loc.located list -> unit
val do_constraint : polymorphic ->
diff --git a/interp/discharge.ml b/interp/discharge.ml
index 0e4bbd299..5b4b5f67b 100644
--- a/interp/discharge.ml
+++ b/interp/discharge.ml
@@ -10,6 +10,7 @@ open Names
open CErrors
open Util
open Term
+open Constr
open Vars
open Declarations
open Cooking
diff --git a/interp/impargs.ml b/interp/impargs.ml
index daec1191e..72d22db4d 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -12,6 +12,7 @@ open Names
open Globnames
open Nameops
open Term
+open Constr
open Reduction
open Declarations
open Environ
@@ -167,7 +168,7 @@ let update pos rig (na,st) =
(* modified is_rigid_reference with a truncated env *)
let is_flexible_reference env bound depth f =
- match kind_of_term f with
+ match kind f with
| Rel n when n >= bound+depth -> (* inductive type *) false
| Rel n when n >= depth -> (* previous argument *) true
| Rel n -> (* since local definitions have been expanded *) false
@@ -191,7 +192,7 @@ let add_free_rels_until strict strongly_strict revpat bound env m pos acc =
let rec frec rig (env,depth as ed) c =
let hd = if strict then whd_all env c else c in
let c = if strongly_strict then hd else c in
- match kind_of_term hd with
+ match kind hd with
| Rel n when (n < bound+depth) && (n >= depth) ->
let i = bound + depth - n - 1 in
acc.(i) <- update pos rig acc.(i)
@@ -214,13 +215,13 @@ let add_free_rels_until strict strongly_strict revpat bound env m pos acc =
let () = if not (Vars.noccur_between 1 bound m) then frec true (env,1) m in
acc
-let rec is_rigid_head t = match kind_of_term t with
+let rec is_rigid_head t = match kind t with
| Rel _ | Evar _ -> false
| Ind _ | Const _ | Var _ | Sort _ -> true
| Case (_,_,f,_) -> is_rigid_head f
| Proj (p,c) -> true
| App (f,args) ->
- (match kind_of_term f with
+ (match kind f with
| Fix ((fi,i),_) -> is_rigid_head (args.(fi.(i)))
| _ -> is_rigid_head f)
| Lambda _ | LetIn _ | Construct _ | CoFix _ | Fix _
@@ -240,7 +241,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
let open Context.Rel.Declaration in
let rec aux env avoid n names t =
let t = whd_all env t in
- match kind_of_term t with
+ match kind t with
| Prod (na,a,b) ->
let na',avoid' = find_displayed_name_in all avoid na (names,b) in
add_free_rels_until strict strongly_strict revpat n env a (Hyp (n+1))
@@ -253,7 +254,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
add_free_rels_until strict strongly_strict revpat n env t Conclusion v
else v
in
- match kind_of_term (whd_all env t) with
+ match kind (whd_all env t) with
| Prod (na,a,b) ->
let na',avoid = find_displayed_name_in all Id.Set.empty na ([],b) in
let v = aux (push_rel (LocalAssum (na',a)) env) avoid 1 [na'] b in
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 658d9e01a..40fa4cb26 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -7,8 +7,8 @@
(************************************************************************)
open Names
+open Constr
open Globnames
-open Term
open Environ
(** {6 Implicit Arguments } *)
diff --git a/interp/notation.ml b/interp/notation.ml
index 076570c8a..f36294f73 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -11,7 +11,7 @@ open CErrors
open Util
open Pp
open Names
-open Term
+open Constr
open Libnames
open Globnames
open Constrexpr
@@ -653,7 +653,7 @@ let find_scope_class_opt = function
(* Special scopes associated to arguments of a global reference *)
let rec compute_arguments_classes t =
- match kind_of_term (EConstr.Unsafe.to_constr (Reductionops.whd_betaiotazeta Evd.empty (EConstr.of_constr t))) with
+ match Constr.kind (EConstr.Unsafe.to_constr (Reductionops.whd_betaiotazeta Evd.empty (EConstr.of_constr t))) with
| Prod (_,t,u) ->
let cl = try Some (compute_scope_class t) with Not_found -> None in
cl :: compute_arguments_classes u
diff --git a/interp/notation.mli b/interp/notation.mli
index e312a3767..2066d346f 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -165,8 +165,8 @@ val subst_scope_class :
val declare_scope_class : scope_name -> scope_class -> unit
val declare_ref_arguments_scope : global_reference -> unit
-val compute_arguments_scope : Term.types -> scope_name option list
-val compute_type_scope : Term.types -> scope_name option
+val compute_arguments_scope : Constr.types -> scope_name option list
+val compute_type_scope : Constr.types -> scope_name option
(** Get the current scope bound to Sortclass, if it exists *)
val current_type_scope_name : unit -> scope_name option
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 16:57:59 +0000