aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/assumptions.ml18
-rw-r--r--vernac/assumptions.mli6
-rw-r--r--vernac/auto_ind_decl.ml36
-rw-r--r--vernac/class.ml7
-rw-r--r--vernac/classes.ml3
-rw-r--r--vernac/classes.mli2
-rw-r--r--vernac/command.ml5
-rw-r--r--vernac/command.mli4
-rw-r--r--vernac/declareDef.mli2
-rw-r--r--vernac/himsg.ml16
-rw-r--r--vernac/indschemes.ml5
-rw-r--r--vernac/indschemes.mli10
-rw-r--r--vernac/lemmas.ml13
-rw-r--r--vernac/lemmas.mli2
-rw-r--r--vernac/obligations.ml33
-rw-r--r--vernac/obligations.mli12
-rw-r--r--vernac/record.ml5
-rw-r--r--vernac/record.mli4
-rw-r--r--vernac/search.ml2
-rw-r--r--vernac/search.mli2
-rw-r--r--vernac/vernacentries.ml9
-rw-r--r--vernac/vernacinterp.ml14
-rw-r--r--vernac/vernacinterp.mli4
23 files changed, 115 insertions, 99 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 6711b14da0..d22024568c 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -18,7 +18,7 @@ open Pp
open CErrors
open Util
open Names
-open Term
+open Constr
open Declarations
open Mod_subst
open Globnames
@@ -89,7 +89,7 @@ and fields_of_mp mp =
let mb = lookup_module_in_impl mp in
let fields,inner_mp,subs = fields_of_mb empty_subst mb [] in
let subs =
- if mp_eq inner_mp mp then subs
+ if ModPath.equal inner_mp mp then subs
else add_mp inner_mp mp mb.mod_delta subs
in
Modops.subst_structure subs fields
@@ -118,7 +118,7 @@ and fields_of_expression x = fields_of_functor fields_of_expr x
let lookup_constant_in_impl cst fallback =
try
- let mp,dp,lab = repr_kn (canonical_con cst) in
+ let mp,dp,lab = KerName.repr (Constant.canonical cst) in
let fields = memoize_fields_of_mp mp in
(* A module found this way is necessarily closed, in particular
our constant cannot be in an opened section : *)
@@ -131,7 +131,7 @@ let lookup_constant_in_impl cst fallback =
- The label has not been found in the structure. This is an error *)
match fallback with
| Some cb -> cb
- | None -> anomaly (str "Print Assumption: unknown constant " ++ pr_con cst ++ str ".")
+ | None -> anomaly (str "Print Assumption: unknown constant " ++ Constant.print cst ++ str ".")
let lookup_constant cst =
try
@@ -142,7 +142,7 @@ let lookup_constant cst =
let lookup_mind_in_impl mind =
try
- let mp,dp,lab = repr_kn (canonical_mind mind) in
+ let mp,dp,lab = KerName.repr (MutInd.canonical mind) in
let fields = memoize_fields_of_mp mp in
search_mind_label lab fields
with Not_found ->
@@ -156,14 +156,14 @@ let lookup_mind mind =
traversed objects *)
let label_of = function
- | ConstRef kn -> pi3 (repr_con kn)
+ | ConstRef kn -> pi3 (Constant.repr3 kn)
| IndRef (kn,_)
- | ConstructRef ((kn,_),_) -> pi3 (repr_mind kn)
+ | ConstructRef ((kn,_),_) -> pi3 (MutInd.repr3 kn)
| VarRef id -> Label.of_id id
let fold_constr_with_full_binders g f n acc c =
let open Context.Rel.Declaration in
- match kind_of_term c with
+ match Constr.kind c with
| Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ -> acc
| Cast (c,_, t) -> f n (f n acc c) t
| Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
@@ -182,7 +182,7 @@ let fold_constr_with_full_binders g f n acc c =
let fd = Array.map2 (fun t b -> (t,b)) tl bl in
Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
-let rec traverse current ctx accu t = match kind_of_term t with
+let rec traverse current ctx accu t = match Constr.kind t with
| Var id ->
let body () = id |> Global.lookup_named |> NamedDecl.get_value in
traverse_object accu body (VarRef id)
diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli
index 46730f8247..afe932ead8 100644
--- a/vernac/assumptions.mli
+++ b/vernac/assumptions.mli
@@ -7,7 +7,7 @@
(************************************************************************)
open Names
-open Term
+open Constr
open Globnames
open Printer
@@ -21,11 +21,11 @@ open Printer
val traverse :
Label.t -> constr ->
(Refset_env.t * Refset_env.t Refmap_env.t *
- (label * Context.Rel.t * types) list Refmap_env.t)
+ (Label.t * Context.Rel.t * types) list Refmap_env.t)
(** Collects all the assumptions (optionally including opaque definitions)
on which a term relies (together with their type). The above warning of
{!traverse} also applies. *)
val assumptions :
?add_opaque:bool -> ?add_transparent:bool -> transparent_state ->
- global_reference -> constr -> Term.types ContextObjectMap.t
+ global_reference -> constr -> types ContextObjectMap.t
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 503508fc04..3cf181441d 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -13,6 +13,7 @@ open CErrors
open Util
open Pp
open Term
+open Constr
open Vars
open Termops
open Declarations
@@ -91,6 +92,15 @@ let destruct_on_using c id =
let destruct_on_as c l =
destruct false None c (Some (Loc.tag l)) None
+let inj_flags = Some {
+ Equality.keep_proof_equalities = true; (* necessary *)
+ injection_in_context = true; (* does not matter here *)
+ Equality.injection_pattern_l2r_order = true; (* does not matter here *)
+ }
+
+let my_discr_tac = Equality.discr_tac false None
+let my_inj_tac x = Equality.inj inj_flags None false None (EConstr.mkVar x,NoBindings)
+
(* reconstruct the inductive with the correct de Bruijn indexes *)
let mkFullInd (ind,u) n =
let mib = Global.lookup_mind (fst ind) in
@@ -181,7 +191,7 @@ let build_beq_scheme mode kn =
match EConstr.kind sigma c with
| Rel x -> mkRel (x-nlist+ndx), Safe_typing.empty_private_constants
| Var x ->
- let eid = id_of_string ("eq_"^(string_of_id x)) in
+ let eid = Id.of_string ("eq_"^(Id.to_string x)) in
let () =
try ignore (Environ.lookup_named eid env)
with Not_found -> raise (ParameterWithoutEquality (VarRef x))
@@ -190,7 +200,7 @@ let build_beq_scheme mode kn =
| Cast (x,_,_) -> aux (EConstr.applist (x,a))
| App _ -> assert false
| Ind ((kn',i as ind'),u) (*FIXME: universes *) ->
- if eq_mind kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Safe_typing.empty_private_constants
+ if MutInd.equal kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Safe_typing.empty_private_constants
else begin
try
let eq, eff =
@@ -358,8 +368,8 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
(* if this happen then the args have to be already declared as a
Parameter*)
(
- let mp,dir,lbl = repr_con (fst (destConst sigma v)) in
- mkConst (make_con mp dir (mk_label (
+ let mp,dir,lbl = Constant.repr3 (fst (destConst sigma v)) in
+ mkConst (Constant.make3 mp dir (Label.make (
if Int.equal offset 1 then ("eq_"^(Label.to_string lbl))
else ((Label.to_string lbl)^"_lb")
)))
@@ -419,8 +429,8 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
(* if this happen then the args have to be already declared as a
Parameter*)
(
- let mp,dir,lbl = repr_con (fst (destConst sigma v)) in
- mkConst (make_con mp dir (mk_label (
+ let mp,dir,lbl = Constant.repr3 (fst (destConst sigma v)) in
+ mkConst (Constant.make3 mp dir (Label.make (
if Int.equal offset 1 then ("eq_"^(Label.to_string lbl))
else ((Label.to_string lbl)^"_bl")
)))
@@ -495,7 +505,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.")
end
end >>= fun (sp2,i2) ->
- if not (eq_mind sp1 sp2) || not (Int.equal i1 i2)
+ if not (MutInd.equal sp1 sp2) || not (Int.equal i1 i2)
then Tacticals.New.tclZEROMSG (str "Eq should be on the same type")
else aux (Array.to_list ca1) (Array.to_list ca2)
@@ -522,8 +532,8 @@ let eqI ind l =
and e, eff =
try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff
with Not_found -> user_err ~hdr:"AutoIndDecl.eqI"
- (str "The boolean equality on " ++ pr_mind (fst ind) ++ str " is needed.");
- in (if Array.equal Term.eq_constr eA [||] then e else mkApp(e,eA)), eff
+ (str "The boolean equality on " ++ MutInd.print (fst ind) ++ str " is needed.");
+ in (if Array.equal Constr.equal eA [||] then e else mkApp(e,eA)), eff
(**********************************************************************)
(* Boolean->Leibniz *)
@@ -595,7 +605,7 @@ let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec =
intro_using freshz;
intros;
Tacticals.New.tclTRY (
- Tacticals.New.tclORELSE reflexivity (Equality.discr_tac false None)
+ Tacticals.New.tclORELSE reflexivity my_discr_tac
);
simpl_in_hyp (freshz,Locus.InHyp);
(*
@@ -739,9 +749,9 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
intro_using freshz;
intros;
Tacticals.New.tclTRY (
- Tacticals.New.tclORELSE reflexivity (Equality.discr_tac false None)
+ Tacticals.New.tclORELSE reflexivity my_discr_tac
);
- Equality.inj None false None (EConstr.mkVar freshz,NoBindings);
+ my_inj_tac freshz;
intros; simpl_in_concl;
Auto.default_auto;
Tacticals.New.tclREPEAT (
@@ -936,7 +946,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
NoBindings
)
true;
- Equality.discr_tac false None
+ my_discr_tac
]
end
]
diff --git a/vernac/class.ml b/vernac/class.ml
index 3915148a08..f26599973e 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -11,6 +11,7 @@ open Util
open Pp
open Names
open Term
+open Constr
open Vars
open Termops
open Entries
@@ -148,7 +149,7 @@ let get_target t ind =
let prods_of t =
- let rec aux acc d = match kind_of_term d with
+ let rec aux acc d = match Constr.kind d with
| Prod (_,c1,c2) -> aux (c1::acc) c2
| Cast (c,_,_) -> aux acc c
| _ -> (d,acc)
@@ -173,8 +174,8 @@ let get_strength stre ref cls clt =
let ident_key_of_class = function
| CL_FUN -> "Funclass"
| CL_SORT -> "Sortclass"
- | CL_CONST sp | CL_PROJ sp -> Label.to_string (con_label sp)
- | CL_IND (sp,_) -> Label.to_string (mind_label sp)
+ | CL_CONST sp | CL_PROJ sp -> Label.to_string (Constant.label sp)
+ | CL_IND (sp,_) -> Label.to_string (MutInd.label sp)
| CL_SECVAR id -> Id.to_string id
(* Identity coercion *)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 0926c93e57..22117f7e15 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -9,6 +9,7 @@
(*i*)
open Names
open Term
+open Constr
open Vars
open Environ
open Nametab
@@ -98,7 +99,7 @@ let type_ctx_instance evars env ctx inst subst =
let id_of_class cl =
match cl.cl_impl with
- | ConstRef kn -> let _,_,l = repr_con kn in Label.to_id l
+ | ConstRef kn -> let _,_,l = Constant.repr3 kn in Label.to_id l
| IndRef (kn,i) ->
let mip = (Environ.lookup_mind kn (Global.env ())).Declarations.mind_packets in
mip.(0).Declarations.mind_typename
diff --git a/vernac/classes.mli b/vernac/classes.mli
index fcdb5c3bc5..c0f03227c4 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -34,7 +34,7 @@ val declare_instance_constant :
bool -> (* polymorphic *)
Evd.evar_map -> (* Universes *)
Constr.t -> (** body *)
- Term.types -> (** type *)
+ Constr.types -> (** type *)
Names.Id.t
val new_instance :
diff --git a/vernac/command.ml b/vernac/command.ml
index f58ed065c6..db3fa19553 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -10,6 +10,7 @@ open Pp
open CErrors
open Util
open Term
+open Constr
open Vars
open Termops
open Environ
@@ -44,7 +45,7 @@ let do_constraint poly l = Declare.do_constraint poly l
let rec under_binders env sigma f n c =
if Int.equal n 0 then f env sigma (EConstr.of_constr c) else
- match kind_of_term c with
+ match Constr.kind c with
| Lambda (x,t,c) ->
mkLambda (x,t,under_binders (push_rel (LocalAssum (x,t)) env) sigma f (n-1) c)
| LetIn (x,b,t,c) ->
@@ -652,7 +653,7 @@ let extract_mutual_inductive_declaration_components indl =
let is_recursive mie =
let rec is_recursive_constructor lift typ =
- match Term.kind_of_term typ with
+ match Constr.kind typ with
| Prod (_,arg,rest) ->
not (EConstr.Vars.noccurn Evd.empty (** FIXME *) lift (EConstr.of_constr arg)) ||
is_recursive_constructor (lift+1) rest
diff --git a/vernac/command.mli b/vernac/command.mli
index afa97aa24f..5415d33080 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -7,7 +7,7 @@
(************************************************************************)
open Names
-open Term
+open Constr
open Entries
open Libnames
open Globnames
@@ -90,7 +90,7 @@ val interp_mutual_inductive :
val declare_mutual_inductive_with_eliminations :
mutual_inductive_entry -> Universes.universe_binders -> one_inductive_impls list ->
- mutual_inductive
+ MutInd.t
(** Entry points for the vernacular commands Inductive and CoInductive *)
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 5dea0ba272..01a87818a3 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -15,5 +15,5 @@ val declare_definition : Id.t -> definition_kind ->
Safe_typing.private_constants Entries.definition_entry -> Universes.universe_binders -> Impargs.manual_implicits ->
Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference
-val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t ->
+val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.UContext.t -> Id.t ->
Safe_typing.private_constants Entries.proof_output -> Constr.types -> Impargs.manual_implicits -> Globnames.global_reference
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 189c47aab9..7b1a948ed0 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -899,11 +899,11 @@ let explain_not_match_error = function
quote (Univ.pr_constraints (Termops.pr_evd_level Evd.empty) cst)
let explain_signature_mismatch l spec why =
- str "Signature components for label " ++ pr_label l ++
+ str "Signature components for label " ++ Label.print l ++
str " do not match:" ++ spc () ++ explain_not_match_error why ++ str "."
let explain_label_already_declared l =
- str "The label " ++ pr_label l ++ str " is already declared."
+ str "The label " ++ Label.print l ++ str " is already declared."
let explain_application_to_not_path _ =
strbrk "A module cannot be applied to another module application or " ++
@@ -933,11 +933,11 @@ let explain_not_equal_module_paths mp1 mp2 =
str "Non equal modules."
let explain_no_such_label l =
- str "No such label " ++ pr_label l ++ str "."
+ str "No such label " ++ Label.print l ++ str "."
let explain_incompatible_labels l l' =
str "Opening and closing labels are not the same: " ++
- pr_label l ++ str " <> " ++ pr_label l' ++ str "!"
+ Label.print l ++ str " <> " ++ Label.print l' ++ str "!"
let explain_not_a_module s =
quote (str s) ++ str " is not a module."
@@ -946,19 +946,19 @@ let explain_not_a_module_type s =
quote (str s) ++ str " is not a module type."
let explain_not_a_constant l =
- quote (pr_label l) ++ str " is not a constant."
+ quote (Label.print l) ++ str " is not a constant."
let explain_incorrect_label_constraint l =
str "Incorrect constraint for label " ++
- quote (pr_label l) ++ str "."
+ quote (Label.print l) ++ str "."
let explain_generative_module_expected l =
- str "The module " ++ pr_label l ++ str " is not generative." ++
+ str "The module " ++ Label.print l ++ str " is not generative." ++
strbrk " Only components of generative modules can be changed" ++
strbrk " using the \"with\" construct."
let explain_label_missing l s =
- str "The field " ++ pr_label l ++ str " is missing in "
+ str "The field " ++ Label.print l ++ str " is missing in "
++ str s ++ str "."
let explain_include_restricted_functor mp =
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 90168843a6..c0ddc7e2ce 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -21,6 +21,7 @@ open Names
open Declarations
open Entries
open Term
+open Constr
open Inductive
open Decl_kinds
open Indrec
@@ -407,7 +408,7 @@ let do_mutual_induction_scheme lnamedepindsort =
let get_common_underlying_mutual_inductive = function
| [] -> assert false
| (id,(mind,i as ind))::l as all ->
- match List.filter (fun (_,(mind',_)) -> not (eq_mind mind mind')) l with
+ match List.filter (fun (_,(mind',_)) -> not (MutInd.equal mind mind')) l with
| (_,ind')::_ ->
raise (RecursionSchemeError (NotMutualInScheme (ind,ind')))
| [] ->
@@ -458,7 +459,7 @@ let build_combined_scheme env schemes =
let find_inductive ty =
let (ctx, arity) = decompose_prod ty in
let (_, last) = List.hd ctx in
- match kind_of_term last with
+ match Constr.kind last with
| App (ind, args) ->
let ind = destInd ind in
let (_,spec) = Inductive.lookup_mind_specif env (fst ind) in
diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli
index 91c4c58255..4b31389ab4 100644
--- a/vernac/indschemes.mli
+++ b/vernac/indschemes.mli
@@ -8,7 +8,7 @@
open Loc
open Names
-open Term
+open Constr
open Environ
open Vernacexpr
@@ -16,9 +16,9 @@ open Vernacexpr
(** Build and register the boolean equalities associated to an inductive type *)
-val declare_beq_scheme : mutual_inductive -> unit
+val declare_beq_scheme : MutInd.t -> unit
-val declare_eq_decidability : mutual_inductive -> unit
+val declare_eq_decidability : MutInd.t -> unit
(** Build and register a congruence scheme for an equality-like inductive type *)
@@ -39,10 +39,10 @@ val do_scheme : (Id.t located option * scheme) list -> unit
(** Combine a list of schemes into a conjunction of them *)
-val build_combined_scheme : env -> constant list -> Evd.evar_map * constr * types
+val build_combined_scheme : env -> Constant.t list -> Evd.evar_map * constr * types
val do_combined_scheme : Id.t located -> Id.t located list -> unit
(** Hook called at each inductive type definition *)
-val declare_default_schemes : mutual_inductive -> unit
+val declare_default_schemes : MutInd.t -> unit
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 9ab89c8832..be9de5b302 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -14,6 +14,7 @@ open Util
open Pp
open Names
open Term
+open Constr
open Declarations
open Declareops
open Entries
@@ -62,7 +63,7 @@ let adjust_guardness_conditions const = function
{ const with const_entry_body =
Future.chain const.const_entry_body
(fun ((body, ctx), eff) ->
- match kind_of_term body with
+ match Constr.kind body with
| Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
(* let possible_indexes =
List.map2 (fun i c -> match i with Some i -> i | None ->
@@ -97,7 +98,7 @@ let find_mutually_recursive_statements thms =
let ind_hyps =
List.flatten (List.map_i (fun i decl ->
let t = RelDecl.get_type decl in
- match kind_of_term t with
+ match Constr.kind t with
| Ind ((kn,_ as ind),u) when
let mind = Global.lookup_mind kn in
mind.mind_finite <> Decl_kinds.CoFinite ->
@@ -107,7 +108,7 @@ let find_mutually_recursive_statements thms =
let ind_ccl =
let cclenv = push_rel_context hyps (Global.env()) in
let whnf_ccl,_ = whd_all_stack cclenv Evd.empty (EConstr.of_constr ccl) in
- match kind_of_term (EConstr.Unsafe.to_constr whnf_ccl) with
+ match Constr.kind (EConstr.Unsafe.to_constr whnf_ccl) with
| Ind ((kn,_ as ind),u) when
let mind = Global.lookup_mind kn in
Int.equal mind.mind_ntypes n && mind.mind_finite == Decl_kinds.CoFinite ->
@@ -116,7 +117,7 @@ let find_mutually_recursive_statements thms =
[] in
ind_hyps,ind_ccl) thms in
let inds_hyps,ind_ccls = List.split inds in
- let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> eq_mind kn kn' in
+ let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> MutInd.equal kn kn' in
(* Check if all conclusions are coinductive in the same type *)
(* (degenerated cartesian product since there is at most one coind ccl) *)
let same_indccl =
@@ -246,7 +247,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t
| Some body ->
let body = norm body in
let k = Kindops.logical_kind_of_goal_kind kind in
- let rec body_i t = match kind_of_term t with
+ let rec body_i t = match Constr.kind t with
| Fix ((nv,0),decls) -> mkFix ((nv,i),decls)
| CoFix (0,decls) -> mkCoFix (i,decls)
| LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2)
@@ -506,7 +507,7 @@ let save_proof ?proof = function
let env = Global.env () in
let ids_typ = Environ.global_vars_set env typ in
let ids_def = Environ.global_vars_set env pproof in
- Some (Environ.keep_hyps env (Idset.union ids_typ ids_def))
+ Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def))
| _ -> None in
let decl = Proof_global.get_universe_decl () in
let evd = Evd.from_ctx universes in
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 1e23c7314b..1f46a385d0 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -7,7 +7,7 @@
(************************************************************************)
open Names
-open Term
+open Constr
open Decl_kinds
type 'a declaration_hook
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 785c842ba1..e231462739 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -13,6 +13,7 @@ open Declare
*)
open Term
+open Constr
open Vars
open Names
open Evd
@@ -55,7 +56,7 @@ let subst_evar_constr evs n idf t =
let seen = ref Int.Set.empty in
let transparent = ref Id.Set.empty in
let evar_info id = List.assoc_f Evar.equal id evs in
- let rec substrec (depth, fixrels) c = match kind_of_term c with
+ let rec substrec (depth, fixrels) c = match Constr.kind c with
| Evar (k, args) ->
let { ev_name = (id, idstr) ;
ev_hyps = hyps ; ev_chop = chop } =
@@ -85,15 +86,15 @@ let subst_evar_constr evs n idf t =
in aux hyps args []
in
if List.exists
- (fun x -> match kind_of_term x with
+ (fun x -> match Constr.kind x with
| Rel n -> Int.List.mem n fixrels
| _ -> false) args
then
transparent := Id.Set.add idstr !transparent;
mkApp (idf idstr, Array.of_list args)
| Fix _ ->
- map_constr_with_binders succfix substrec (depth, 1 :: fixrels) c
- | _ -> map_constr_with_binders succfix substrec (depth, fixrels) c
+ Constr.map_with_binders succfix substrec (depth, 1 :: fixrels) c
+ | _ -> Constr.map_with_binders succfix substrec (depth, fixrels) c
in
let t' = substrec (0, []) t in
t', !seen, !transparent
@@ -103,9 +104,9 @@ let subst_evar_constr evs n idf t =
where n binders were passed through. *)
let subst_vars acc n t =
let var_index id = Util.List.index Id.equal id acc in
- let rec substrec depth c = match kind_of_term c with
+ let rec substrec depth c = match Constr.kind c with
| Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c)
- | _ -> map_constr_with_binders succ substrec depth c
+ | _ -> Constr.map_with_binders succ substrec depth c
in
substrec 0 t
@@ -144,7 +145,7 @@ let rec chop_product n t =
let pop t = Vars.lift (-1) t in
if Int.equal n 0 then Some t
else
- match kind_of_term t with
+ match Constr.kind t with
| Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (pop b) else None
| _ -> None
@@ -273,7 +274,7 @@ let explain_no_obligations = function
| None -> str "No obligations remaining"
type obligation_info =
- (Names.Id.t * Term.types * Evar_kinds.t Loc.located *
+ (Names.Id.t * types * Evar_kinds.t Loc.located *
(bool * Evar_kinds.obligation_definition_status)
* Int.Set.t * unit Proofview.tactic option) array
@@ -384,7 +385,7 @@ let subst_deps expand obls deps t =
(Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t)
let rec prod_app t n =
- match kind_of_term (EConstr.Unsafe.to_constr (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) (** FIXME *) with
+ match Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) (** FIXME *) with
| Prod (_,_,b) -> subst1 n b
| LetIn (_, b, t, b') -> prod_app (subst1 b b') n
| _ ->
@@ -400,13 +401,13 @@ let replace_appvars subst =
let f, l = decompose_app c in
if isVar f then
try
- let c' = List.map (map_constr aux) l in
+ let c' = List.map (Constr.map aux) l in
let (t, b) = Id.List.assoc (destVar f) subst in
mkApp (delayed_force hide_obligation,
[| prod_applist t c'; applistc b c' |])
- with Not_found -> map_constr aux c
- else map_constr aux c
- in map_constr aux
+ with Not_found -> Constr.map aux c
+ else Constr.map aux c
+ in Constr.map aux
let subst_prog expand obls ints prg =
let subst = obl_substitution expand obls ints in
@@ -490,7 +491,7 @@ let declare_definition prg =
cst
let rec lam_index n t acc =
- match kind_of_term t with
+ match Constr.kind t with
| Lambda (Name n', _, _) when Id.equal n n' ->
acc
| Lambda (_, _, b) ->
@@ -566,9 +567,9 @@ let declare_mutual_definition l =
let decompose_lam_prod c ty =
let open Context.Rel.Declaration in
let rec aux ctx c ty =
- match kind_of_term c, kind_of_term ty with
+ match Constr.kind c, Constr.kind ty with
| LetIn (x, b, t, c), LetIn (x', b', t', ty)
- when eq_constr b b' && eq_constr t t' ->
+ when Constr.equal b b' && Constr.equal t t' ->
let ctx' = Context.Rel.add (LocalDef (x,b',t')) ctx in
aux ctx' c ty
| _, LetIn (x', b', t', ty) ->
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 11c2553ae1..d037fdcd8a 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -7,7 +7,7 @@
(************************************************************************)
open Environ
-open Term
+open Constr
open Evd
open Names
open Globnames
@@ -39,7 +39,7 @@ val eterm_obligations : env -> Id.t -> evar_map -> int ->
translation from obligation identifiers to constrs, new term, new type *)
type obligation_info =
- (Id.t * Term.types * Evar_kinds.t Loc.located *
+ (Id.t * types * Evar_kinds.t Loc.located *
(bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array
(* ident, type, location, (opaque or transparent, expand or define),
dependencies, tactic to solve it *)
@@ -51,13 +51,13 @@ type progress = (* Resolution status of a program *)
val default_tactic : unit Proofview.tactic ref
-val add_definition : Names.Id.t -> ?term:Term.constr -> Term.types ->
+val add_definition : Names.Id.t -> ?term:constr -> types ->
Evd.evar_universe_context ->
?univdecl:Univdecls.universe_decl -> (* Universe binders and constraints *)
?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list ->
?kind:Decl_kinds.definition_kind ->
?tactic:unit Proofview.tactic ->
- ?reduce:(Term.constr -> Term.constr) ->
+ ?reduce:(constr -> constr) ->
?hook:(Evd.evar_universe_context -> unit) Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress
type notations =
@@ -68,13 +68,13 @@ type fixpoint_kind =
| IsCoFixpoint
val add_mutual_definitions :
- (Names.Id.t * Term.constr * Term.types *
+ (Names.Id.t * constr * types *
(Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list ->
Evd.evar_universe_context ->
?univdecl:Univdecls.universe_decl -> (* Universe binders and constraints *)
?tactic:unit Proofview.tactic ->
?kind:Decl_kinds.definition_kind ->
- ?reduce:(Term.constr -> Term.constr) ->
+ ?reduce:(constr -> constr) ->
?hook:(Evd.evar_universe_context -> unit) Lemmas.declaration_hook -> ?opaque:bool ->
notations ->
fixpoint_kind -> unit
diff --git a/vernac/record.ml b/vernac/record.ml
index 5533fe5b38..1fd43624a3 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -13,6 +13,7 @@ open Names
open Globnames
open Nameops
open Term
+open Constr
open Vars
open Environ
open Declarations
@@ -229,7 +230,7 @@ exception NotDefinable of record_error
let subst_projection fid l c =
let lv = List.length l in
let bad_projs = ref [] in
- let rec substrec depth c = match kind_of_term c with
+ let rec substrec depth c = match Constr.kind c with
| Rel k ->
(* We are in context [[params;fields;x:ind;...depth...]] *)
if k <= depth+1 then
@@ -244,7 +245,7 @@ let subst_projection fid l c =
" field which has no name.")
else
mkRel (k-lv)
- | _ -> map_constr_with_binders succ substrec depth c
+ | _ -> Constr.map_with_binders succ substrec depth c
in
let c' = lift 1 c in (* to get [c] defined in ctxt [[params;fields;x:ind]] *)
let c'' = substrec 0 c' in
diff --git a/vernac/record.mli b/vernac/record.mli
index aea474581e..33c2fba89c 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -7,7 +7,7 @@
(************************************************************************)
open Names
-open Term
+open Constr
open Vernacexpr
open Constrexpr
open Impargs
@@ -22,7 +22,7 @@ val primitive_flag : bool ref
val declare_projections :
inductive -> ?kind:Decl_kinds.definition_object_kind -> Id.t ->
coercion_flag list -> manual_explicitation list list -> Context.Rel.t ->
- (Name.t * bool) list * constant option list
+ (Name.t * bool) list * Constant.t option list
val declare_structure :
Decl_kinds.recursivity_kind ->
diff --git a/vernac/search.ml b/vernac/search.ml
index 0f56f81e74..6da6a0c2dc 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -9,7 +9,7 @@
open Pp
open Util
open Names
-open Term
+open Constr
open Declarations
open Libobject
open Environ
diff --git a/vernac/search.mli b/vernac/search.mli
index db54d732b6..2eda3980a5 100644
--- a/vernac/search.mli
+++ b/vernac/search.mli
@@ -7,7 +7,7 @@
(************************************************************************)
open Names
-open Term
+open Constr
open Environ
open Pattern
open Globnames
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e08cb83871..7eedf24f82 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -250,7 +250,7 @@ let print_namespace ns =
let print_list pr l = prlist_with_sep (fun () -> str".") pr l in
let print_kn kn =
(* spiwack: I'm ignoring the dirpath, is that bad? *)
- let (mp,_,lbl) = Names.repr_kn kn in
+ let (mp,_,lbl) = Names.KerName.repr kn in
let qn = (qualified_minus (List.length ns) mp)@[Names.Label.to_id lbl] in
print_list pr_id qn
in
@@ -265,8 +265,8 @@ let print_namespace ns =
let constants = (Environ.pre_env (Global.env ())).Pre_env.env_globals.Pre_env.env_constants in
let constants_in_namespace =
Cmap_env.fold (fun c (body,_) acc ->
- let kn = user_con c in
- if matches (modpath kn) then
+ let kn = Constant.user c in
+ if matches (KerName.modpath kn) then
acc++fnl()++hov 2 (print_constant kn body)
else
acc
@@ -1853,7 +1853,6 @@ let vernac_show = let open Feedback in function
| OpenSubgoals -> pr_open_subgoals ()
| NthGoal n -> pr_nth_open_subgoal n
| GoalId id -> pr_goal_by_id id
- | GoalUid id -> pr_goal_by_uid id
in
msg_notice info
| ShowProof -> show_proof ()
@@ -2070,7 +2069,7 @@ let interp ?proof ?loc locality poly c =
| VernacProofMode mn -> Proof_global.set_proof_mode mn [@ocaml.warning "-3"]
(* Extensions *)
- | VernacExtend (opn,args) -> Vernacinterp.call ?locality (opn,args)
+ | VernacExtend (opn,args) -> Vernacinterp.call ?locality ?loc (opn,args)
(* Vernaculars that take a locality flag *)
let check_vernac_supports_locality c l =
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 2d9c0fa362..41fee6bd08 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -11,7 +11,7 @@ open Pp
open CErrors
type deprecation = bool
-type vernac_command = Genarg.raw_generic_argument list -> unit -> unit
+type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit
(* Table of vernac entries *)
let vernac_tab =
@@ -49,8 +49,8 @@ let warn_deprecated_command =
(* Interpretation of a vernac command *)
-let call ?locality (opn,converted_args) =
- let loc = ref "Looking up command" in
+let call ?locality ?loc (opn,converted_args) =
+ let phase = ref "Looking up command" in
try
let depr, callback = vinterp_map opn in
let () = if depr then
@@ -62,16 +62,16 @@ let call ?locality (opn,converted_args) =
let pr = pr_sequence pr_gram rules in
warn_deprecated_command pr;
in
- loc:= "Checking arguments";
+ phase := "Checking arguments";
let hunk = callback converted_args in
- loc:= "Executing command";
+ phase := "Executing command";
Locality.LocalityFixme.set locality;
- hunk();
+ hunk loc;
Locality.LocalityFixme.assert_consumed()
with
| Drop -> raise Drop
| reraise ->
let reraise = CErrors.push reraise in
if !Flags.debug then
- Feedback.msg_debug (str"Vernac Interpreter " ++ str !loc);
+ Feedback.msg_debug (str"Vernac Interpreter " ++ str !phase);
iraise reraise
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index f58d070864..84370fdc29 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -9,7 +9,7 @@
(** Interpretation of extended vernac phrases. *)
type deprecation = bool
-type vernac_command = Genarg.raw_generic_argument list -> unit -> unit
+type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit
val vinterp_add : deprecation -> Vernacexpr.extend_name ->
vernac_command -> unit
@@ -17,4 +17,4 @@ val overwriting_vinterp_add :
Vernacexpr.extend_name -> vernac_command -> unit
val vinterp_init : unit -> unit
-val call : ?locality:bool -> Vernacexpr.extend_name * Genarg.raw_generic_argument list -> unit
+val call : ?locality:bool -> ?loc:Loc.t -> Vernacexpr.extend_name * Genarg.raw_generic_argument list -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 11:30:01 +0000