aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml50
-rw-r--r--interp/constrextern.mli4
-rw-r--r--interp/constrintern.mli2
-rw-r--r--interp/declare.ml30
-rw-r--r--interp/declare.mli12
-rw-r--r--interp/discharge.ml1
-rw-r--r--interp/dumpglob.ml2
-rw-r--r--interp/dumpglob.mli6
-rw-r--r--interp/genintern.ml2
-rw-r--r--interp/impargs.ml17
-rw-r--r--interp/impargs.mli6
-rw-r--r--interp/interp.mllib1
-rw-r--r--interp/notation.ml6
-rw-r--r--interp/notation.mli6
-rw-r--r--interp/stdarg.ml2
-rw-r--r--interp/stdarg.mli2
-rw-r--r--interp/syntax_def.mli2
-rw-r--r--interp/tactypes.ml33
18 files changed, 115 insertions, 69 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index f1bee65ef8..e1cf8f196d 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
@@ -1120,7 +1120,11 @@ let any_any_branch =
(* | _ => _ *)
Loc.tag ([],[DAst.make @@ PatVar Anonymous], DAst.make @@ GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None))
-let rec glob_of_pat env sigma pat = DAst.make @@ match pat with
+let compute_displayed_name_in_pattern sigma avoid na c =
+ let open Namegen in
+ compute_displayed_name_in_gen (fun _ -> Patternops.noccurn_pattern) sigma avoid na c
+
+let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
| PRef ref -> GRef (ref,None)
| PVar id -> GVar id
| PEvar (evk,l) ->
@@ -1130,7 +1134,7 @@ let rec glob_of_pat env sigma pat = DAst.make @@ match pat with
| None -> Id.of_string "__"
| Some id -> id
in
- GEvar (id,List.map (on_snd (glob_of_pat env sigma)) l)
+ GEvar (id,List.map (on_snd (glob_of_pat avoid env sigma)) l)
| PRel n ->
let id = try match lookup_name_of_rel n env with
| Name id -> id
@@ -1141,30 +1145,36 @@ let rec glob_of_pat env sigma pat = DAst.make @@ match pat with
| PMeta None -> GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None)
| PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n)
| PProj (p,c) -> GApp (DAst.make @@ GRef (ConstRef (Projection.constant p),None),
- [glob_of_pat env sigma c])
+ [glob_of_pat avoid env sigma c])
| PApp (f,args) ->
- GApp (glob_of_pat env sigma f,Array.map_to_list (glob_of_pat env sigma) args)
+ GApp (glob_of_pat avoid env sigma f,Array.map_to_list (glob_of_pat avoid env sigma) args)
| PSoApp (n,args) ->
GApp (DAst.make @@ GPatVar (Evar_kinds.SecondOrderPatVar n),
- List.map (glob_of_pat env sigma) args)
+ List.map (glob_of_pat avoid env sigma) args)
| PProd (na,t,c) ->
- GProd (na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c)
+ let na',avoid' = compute_displayed_name_in_pattern sigma avoid na c in
+ let env' = Termops.add_name na' env in
+ GProd (na',Explicit,glob_of_pat avoid env sigma t,glob_of_pat avoid' env' sigma c)
| PLetIn (na,b,t,c) ->
- GLetIn (na,glob_of_pat env sigma b, Option.map (glob_of_pat env sigma) t,
- glob_of_pat (na::env) sigma c)
+ let na',avoid' = Namegen.compute_displayed_let_name_in sigma Namegen.RenamingForGoal avoid na c in
+ let env' = Termops.add_name na' env in
+ GLetIn (na',glob_of_pat avoid env sigma b, Option.map (glob_of_pat avoid env sigma) t,
+ glob_of_pat avoid' env' sigma c)
| PLambda (na,t,c) ->
- GLambda (na,Explicit,glob_of_pat env sigma t, glob_of_pat (na::env) sigma c)
+ let na',avoid' = compute_displayed_name_in_pattern sigma avoid na c in
+ let env' = Termops.add_name na' env in
+ GLambda (na',Explicit,glob_of_pat avoid env sigma t, glob_of_pat avoid' env' sigma c)
| PIf (c,b1,b2) ->
- GIf (glob_of_pat env sigma c, (Anonymous,None),
- glob_of_pat env sigma b1, glob_of_pat env sigma b2)
+ GIf (glob_of_pat avoid env sigma c, (Anonymous,None),
+ glob_of_pat avoid env sigma b1, glob_of_pat avoid env sigma b2)
| PCase ({cip_style=LetStyle; cip_ind_tags=None},PMeta None,tm,[(0,n,b)]) ->
- let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat env sigma b) in
- GLetTuple (nal,(Anonymous,None),glob_of_pat env sigma tm,b)
+ let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat avoid env sigma b) in
+ GLetTuple (nal,(Anonymous,None),glob_of_pat avoid env sigma tm,b)
| PCase (info,p,tm,bl) ->
let mat = match bl, info.cip_ind with
| [], _ -> []
| _, Some ind ->
- let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat env sigma c)) bl in
+ let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat avoid env sigma c)) bl in
simple_cases_matrix_of_branches ind bl'
| _, None -> anomaly (Pp.str "PCase with some branches but unknown inductive.")
in
@@ -1173,16 +1183,16 @@ let rec glob_of_pat env sigma pat = DAst.make @@ match pat with
let indnames,rtn = match p, info.cip_ind, info.cip_ind_tags with
| PMeta None, _, _ -> (Anonymous,None),None
| _, Some ind, Some nargs ->
- return_type_of_predicate ind nargs (glob_of_pat env sigma p)
+ return_type_of_predicate ind nargs (glob_of_pat avoid env sigma p)
| _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.")
in
- GCases (RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat)
- | PFix f -> DAst.get (Detyping.detype_names false Id.Set.empty env (Global.env()) sigma (EConstr.of_constr (mkFix f))) (** FIXME bad env *)
- | PCoFix c -> DAst.get (Detyping.detype_names false Id.Set.empty env (Global.env()) sigma (EConstr.of_constr (mkCoFix c)))
+ GCases (RegularStyle,rtn,[glob_of_pat avoid env sigma tm,indnames],mat)
+ | PFix f -> DAst.get (Detyping.detype_names false avoid env (Global.env()) sigma (EConstr.of_constr (mkFix f))) (** FIXME bad env *)
+ | PCoFix c -> DAst.get (Detyping.detype_names false avoid env (Global.env()) sigma (EConstr.of_constr (mkCoFix c)))
| PSort s -> GSort s
let extern_constr_pattern env sigma pat =
- extern true (None,[]) Id.Set.empty (glob_of_pat env sigma pat)
+ extern true (None,[]) Id.Set.empty (glob_of_pat Id.Set.empty env sigma pat)
let extern_rel_context where env sigma sign =
let a = detype_rel_context Detyping.Later where Id.Set.empty (names_of_rel_context env,env) sigma sign in
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 593580fb7e..d980b1995f 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Names
-open Term
open Termops
open EConstr
open Environ
@@ -19,6 +18,7 @@ open Constrexpr
open Notation_term
open Notation
open Misctypes
+open Ltac_pretype
(** Translation of pattern, cases pattern, glob_constr and term into syntax
trees for printing *)
@@ -40,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 75e99dd9b1..46f96d20b4 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 7fcb38296f..0cc4d0fcaa 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
@@ -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
@@ -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,13 +458,13 @@ 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
let glob', ctx =
List.fold_left (fun ((idl,lid),ctx) (id, lev) ->
- ((Idmap.add id (p, lev) idl,
+ ((Id.Map.add id (p, lev) idl,
Univ.LMap.add lev id lid),
Univ.ContextSet.add_universe lev ctx))
(glob, Univ.ContextSet.empty) l
@@ -525,7 +525,7 @@ let do_constraint poly l =
(str "Cannot declare constraints on anonymous universes")
| GType (Some (loc, Name id)) ->
let names, _ = Global.global_universe_names () in
- try loc, Idmap.find id names
+ try loc, Id.Map.find id names
with Not_found ->
user_err ?loc ~hdr:"Constraint" (str "Undeclared universe " ++ pr_id id)
in
diff --git a/interp/declare.mli b/interp/declare.mli
index ccd7d28bb5..9b3194dec5 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
@@ -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
@@ -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 0e4bbd2993..5b4b5f67b8 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/dumpglob.ml b/interp/dumpglob.ml
index 561b0078aa..13ed65056d 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 afcd7a2ed2..f3ad50f288 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/genintern.ml b/interp/genintern.ml
index f4996c997f..2f2edab30c 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -10,7 +10,7 @@ open Names
open Mod_subst
open Genarg
-module Store = Store.Make(struct end)
+module Store = Store.Make ()
type glob_sign = {
ltacvars : Id.Set.t;
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 09a0ba83ca..72d22db4d9 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
@@ -483,8 +484,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 4b78f54eac..40fa4cb260 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 } *)
@@ -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/interp.mllib b/interp/interp.mllib
index 6d290a325c..e3500cfeac 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -1,3 +1,4 @@
+Tactypes
Stdarg
Genintern
Constrexpr_ops
diff --git a/interp/notation.ml b/interp/notation.ml
index d3cac1e3e9..f36294f732 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
@@ -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) *)
@@ -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 75c8d5aa5f..2066d346fe 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
@@ -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
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 45dec5112b..65c55a584a 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -28,7 +28,7 @@ let wit_string : string uniform_genarg_type =
make0 "string"
let wit_pre_ident : string uniform_genarg_type =
- make0 ~dyn:(val_tag (topwit wit_string)) "preident"
+ make0 "preident"
let loc_of_or_by_notation f = function
| AN c -> f c
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index dffbd6659f..ed00fe2967 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -51,7 +51,7 @@ val wit_sort_family : (Sorts.family, unit, unit) genarg_type
val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
-val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type
+val wit_uconstr : (constr_expr , glob_constr_and_expr, Ltac_pretype.closed_glob_constr) genarg_type
val wit_open_constr :
(constr_expr, glob_constr_and_expr, constr) genarg_type
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 36a3986b54..4d2cb5b74b 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
diff --git a/interp/tactypes.ml b/interp/tactypes.ml
new file mode 100644
index 0000000000..2c42e13110
--- /dev/null
+++ b/interp/tactypes.ml
@@ -0,0 +1,33 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** Tactic-related types that are not totally Ltac specific and still used in
+ lower API. It's not clear whether this is a temporary API or if this is
+ meant to stay. *)
+
+open Loc
+open Names
+open Constrexpr
+open Pattern
+open Misctypes
+
+(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
+ in the environment by the effective calls to Intro, Inversion, etc
+ The [constr_expr] field is [None] in TacDef though *)
+type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option
+type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * constr_pattern
+
+type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a
+
+type delayed_open_constr = EConstr.constr delayed_open
+type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open
+
+type intro_pattern = delayed_open_constr intro_pattern_expr located
+type intro_patterns = delayed_open_constr intro_pattern_expr located list
+type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr located
+type intro_pattern_naming = intro_pattern_naming_expr located
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 04:54:41 +0000