aboutsummaryrefslogtreecommitdiff
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.ml26
-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/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/syntax_def.mli2
-rw-r--r--interp/tactypes.ml33
15 files changed, 80 insertions, 45 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index bd6aa09111..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
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index b2df449c59..d980b1995f 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 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 bd8f3db507..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,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 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/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/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-03-09 07:18:59 +0000