aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/arguments_renaming.ml5
-rw-r--r--pretyping/cases.ml60
-rw-r--r--pretyping/coercion.ml1
-rw-r--r--pretyping/evarconv.ml3
-rw-r--r--pretyping/evardefine.ml8
-rw-r--r--pretyping/find_subterm.ml4
-rw-r--r--pretyping/nativenorm.ml4
-rw-r--r--pretyping/pretyping.ml13
-rw-r--r--pretyping/retyping.ml10
-rw-r--r--pretyping/tacred.ml24
-rw-r--r--pretyping/typeclasses.ml14
-rw-r--r--pretyping/unification.ml17
-rw-r--r--pretyping/vnorm.ml8
13 files changed, 91 insertions, 80 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index fe10737623..ff6b33c491 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -13,6 +13,8 @@ open Term
open Environ
open Util
open Libobject
+
+module NamedDecl = Context.Named.Declaration
(*i*)
let name_table =
@@ -48,8 +50,7 @@ let discharge_rename_args = function
(try
let vars,_,_ = section_segment_of_reference c in
let c' = pop_global_reference c in
- let open Context.Named.Declaration in
- let var_names = List.map (Name.mk_name % get_id % fst) vars in
+ let var_names = List.map (Name.mk_name % NamedDecl.get_id % fst) vars in
let names' = List.map (fun l -> var_names @ l) names in
Some (ReqGlobal (c', names), (c', names'))
with Not_found -> Some req)
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index fe2b0a5a1a..2d8173f944 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -32,6 +32,9 @@ open Evd
open Sigma.Notations
open Context.Rel.Declaration
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
(* Pattern-matching errors *)
type pattern_matching_error =
@@ -605,7 +608,7 @@ let relocate_index_tomatch n1 n2 =
NonDepAlias :: genrec depth rest
| Abstract (i,d) :: rest ->
let i = relocate_rel n1 n2 depth i in
- Abstract (i, map_constr (relocate_index n1 n2 depth) d)
+ Abstract (i, RelDecl.map_constr (relocate_index n1 n2 depth) d)
:: genrec (depth+1) rest in
genrec 0
@@ -638,7 +641,7 @@ let replace_tomatch n c =
| NonDepAlias :: rest ->
NonDepAlias :: replrec depth rest
| Abstract (i,d) :: rest ->
- Abstract (i, map_constr (replace_term n c depth) d)
+ Abstract (i, RelDecl.map_constr (replace_term n c depth) d)
:: replrec (depth+1) rest in
replrec 0
@@ -663,7 +666,7 @@ let rec liftn_tomatch_stack n depth = function
NonDepAlias :: liftn_tomatch_stack n depth rest
| Abstract (i,d)::rest ->
let i = if i<depth then i else i+n in
- Abstract (i, map_constr (liftn n depth) d)
+ Abstract (i, RelDecl.map_constr (liftn n depth) d)
::(liftn_tomatch_stack n (depth+1) rest)
let lift_tomatch_stack n = liftn_tomatch_stack n 1
@@ -731,7 +734,7 @@ let get_names env sign eqns =
(* We now replace the names y1 .. yn y by the actual names *)
(* xi1 .. xin xi to be found in the i-th clause of the matrix *)
-let recover_initial_subpattern_names = List.map2 set_name
+let recover_initial_subpattern_names = List.map2 RelDecl.set_name
let recover_and_adjust_alias_names names sign =
let rec aux = function
@@ -756,11 +759,11 @@ let push_rels_eqn_with_names sign eqn =
push_rels_eqn sign eqn
let push_generalized_decl_eqn env n decl eqn =
- match get_name decl with
+ match RelDecl.get_name decl with
| Anonymous ->
push_rels_eqn [decl] eqn
| Name _ ->
- push_rels_eqn [set_name (get_name (Environ.lookup_rel n eqn.rhs.rhs_env)) decl] eqn
+ push_rels_eqn [RelDecl.set_name (RelDecl.get_name (Environ.lookup_rel n eqn.rhs.rhs_env)) decl] eqn
let drop_alias_eqn eqn =
{ eqn with alias_stack = List.tl eqn.alias_stack }
@@ -768,7 +771,7 @@ let drop_alias_eqn eqn =
let push_alias_eqn alias eqn =
let aliasname = List.hd eqn.alias_stack in
let eqn = drop_alias_eqn eqn in
- let alias = set_name aliasname alias in
+ let alias = RelDecl.set_name aliasname alias in
push_rels_eqn [alias] eqn
(**********************************************************************)
@@ -1195,7 +1198,7 @@ let rec generalize_problem names pb = function
| LocalDef (Anonymous,_,_) -> pb', deps
| _ ->
(* for better rendering *)
- let d = map_type (whd_betaiota !(pb.evdref)) d in
+ let d = RelDecl.map_type (whd_betaiota !(pb.evdref)) d in
let tomatch = lift_tomatch_stack 1 pb'.tomatch in
let tomatch = relocate_index_tomatch (i+1) 1 tomatch in
{ pb' with
@@ -1223,7 +1226,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
(* that had matched constructor C *)
let cs_args = const_info.cs_args in
let names,aliasname = get_names pb.env cs_args eqns in
- let typs = List.map2 set_name names cs_args
+ let typs = List.map2 RelDecl.set_name names cs_args
in
(* We build the matrix obtained by expanding the matching on *)
@@ -1273,7 +1276,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
let typs' =
List.map2
(fun (tm, (tmtyp,_), decl) deps ->
- let na = get_name decl in
+ let na = RelDecl.get_name decl in
let na = match curname, na with
| Name _, Anonymous -> curname
| Name _, Name _ -> na
@@ -1658,8 +1661,7 @@ let abstract_tycon loc env evdref subst tycon extenv t =
List.map (fun a -> not (isRel a) || dependent a u
|| Int.Set.mem (destRel a) depvl) inst in
let named_filter =
- let open Context.Named.Declaration in
- List.map (fun d -> dependent (mkVar (get_id d)) u)
+ List.map (fun d -> dependent (mkVar (NamedDecl.get_id d)) u)
(named_context extenv) in
let filter = Filter.make (rel_filter @ named_filter) in
let candidates = u :: List.map mkRel vl in
@@ -1755,7 +1757,7 @@ let build_inversion_problem loc env sigma tms t =
let sub_tms =
List.map2 (fun deps (tm, (tmtyp,_), decl) ->
- let na = if List.is_empty deps then Anonymous else force_name (get_name decl) in
+ let na = if List.is_empty deps then Anonymous else force_name (RelDecl.get_name decl) in
Pushed (true,((tm,tmtyp),deps,na)))
dep_sign decls in
let subst = List.map (fun (na,t) -> (na,lift n t)) subst in
@@ -1818,7 +1820,7 @@ let build_initial_predicate arsign pred =
let rec buildrec n pred tmnames = function
| [] -> List.rev tmnames,pred
| (decl::realdecls)::lnames ->
- let na = get_name decl in
+ let na = RelDecl.get_name decl in
let n' = n + List.length realdecls in
buildrec (n'+1) pred (force_name na::tmnames) lnames
| _ -> assert false
@@ -1851,7 +1853,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
List.rev realnal
| None -> List.make nrealargs_ctxt Anonymous in
LocalAssum (na, build_dependent_inductive env0 indf')
- ::(List.map2 set_name realnal arsign) in
+ ::(List.map2 RelDecl.set_name realnal arsign) in
let rec buildrec n = function
| [],[] -> []
| (_,tm)::ltm, (_,x)::tmsign ->
@@ -2048,7 +2050,7 @@ let constr_of_pat env evdref arsign pat avoid =
let patargs, args, sign, env, n, m, avoid =
List.fold_right2
(fun decl ua (patargs, args, sign, env, n, m, avoid) ->
- let t = get_type decl in
+ let t = RelDecl.get_type decl in
let pat', sign', arg', typ', argtypargs, n', avoid =
let liftt = liftn (List.length sign) (succ (List.length args)) t in
typ env (substl args liftt, []) ua avoid
@@ -2088,8 +2090,8 @@ let constr_of_pat env evdref arsign pat avoid =
(* Mark the equality as a hole *)
pat', sign, lift i app, lift i apptype, realargs, n + i, avoid
in
- let pat', sign, patc, patty, args, z, avoid = typ env (get_type (List.hd arsign), List.tl arsign) pat avoid in
- pat', (sign, patc, (get_type (List.hd arsign), args), pat'), avoid
+ let pat', sign, patc, patty, args, z, avoid = typ env (RelDecl.get_type (List.hd arsign), List.tl arsign) pat avoid in
+ pat', (sign, patc, (RelDecl.get_type (List.hd arsign), args), pat'), avoid
(* shadows functional version *)
@@ -2120,7 +2122,7 @@ let vars_of_ctx ctx =
(GRef (Loc.ghost, delayed_force coq_eq_refl_ref, None)),
[hole; GVar (Loc.ghost, prev)])) :: vars
| _ ->
- match get_name decl with
+ match RelDecl.get_name decl with
Anonymous -> invalid_arg "vars_of_ctx"
| Name n -> n, GVar (Loc.ghost, n) :: vars)
ctx (Id.of_string "vars_of_ctx_error", [])
@@ -2297,7 +2299,7 @@ let abstract_tomatch env tomatchs tycon =
let build_dependent_signature env evdref avoid tomatchs arsign =
let avoid = ref avoid in
let arsign = List.rev arsign in
- let allnames = List.rev_map (List.map get_name) arsign in
+ let allnames = List.rev_map (List.map RelDecl.get_name) arsign in
let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in
let eqs, neqs, refls, slift, arsign' =
List.fold_left2
@@ -2314,14 +2316,14 @@ let build_dependent_signature env evdref avoid tomatchs arsign =
as much as possible *)
let argsign = List.tl arsign in (* arguments in inverse application order *)
let app_decl = List.hd arsign in (* The matched argument *)
- let appn = get_name app_decl in
- let appt = get_type app_decl in
+ let appn = RelDecl.get_name app_decl in
+ let appt = RelDecl.get_type app_decl in
let argsign = List.rev argsign in (* arguments in application order *)
let env', nargeqs, argeqs, refl_args, slift, argsign' =
List.fold_left2
(fun (env, nargeqs, argeqs, refl_args, slift, argsign') arg decl ->
- let name = get_name decl in
- let t = get_type decl in
+ let name = RelDecl.get_name decl in
+ let t = RelDecl.get_type decl in
let argt = Retyping.get_type_of env !evdref arg in
let eq, refl_arg =
if Reductionops.is_conv env !evdref argt t then
@@ -2339,7 +2341,7 @@ let build_dependent_signature env evdref avoid tomatchs arsign =
let previd, id =
let name =
match kind_of_term arg with
- Rel n -> get_name (lookup_rel n env)
+ Rel n -> RelDecl.get_name (lookup_rel n env)
| _ -> name
in
make_prime avoid name
@@ -2348,7 +2350,7 @@ let build_dependent_signature env evdref avoid tomatchs arsign =
(LocalAssum (Name (eq_id avoid previd), eq)) :: argeqs,
refl_arg :: refl_args,
pred slift,
- set_name (Name id) decl :: argsign'))
+ RelDecl.set_name (Name id) decl :: argsign'))
(env, neqs, [], [], slift, []) args argsign
in
let eq = mk_JMeq evdref
@@ -2363,13 +2365,13 @@ let build_dependent_signature env evdref avoid tomatchs arsign =
succ nargeqs,
refl_eq :: refl_args,
pred slift,
- ((set_name (Name id) app_decl :: argsign') :: arsigns))
+ ((RelDecl.set_name (Name id) app_decl :: argsign') :: arsigns))
| _ -> (* Non dependent inductive or not inductive, just use a regular equality *)
let decl = match arsign with [x] -> x | _ -> assert(false) in
- let name = get_name decl in
+ let name = RelDecl.get_name decl in
let previd, id = make_prime avoid name in
- let arsign' = set_name (Name id) decl in
+ let arsign' = RelDecl.set_name (Name id) decl in
let tomatch_ty = type_of_tomatch ty in
let eq =
mk_eq evdref (lift nar tomatch_ty)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 913e80f399..553786f589 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -153,7 +153,6 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
and coerce' env x y : (Term.constr -> Term.constr) option =
let subco () = subset_coerce env evdref x y in
let dest_prod c =
- let open Context.Rel.Declaration in
match Reductionops.splay_prod_n env ( !evdref) 1 c with
| [LocalAssum (na,t) | LocalDef (na,_,t)], c -> (na,t), c
| _ -> raise NoSubtacCoercion
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 2f73ddd30c..e745824b8a 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -24,6 +24,7 @@ open Globnames
open Evd
open Pretype_errors
open Sigma.Notations
+open Context.Named.Declaration
module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
@@ -962,7 +963,7 @@ let apply_on_subterm env evdref f c t =
match kind_of_term t with
| Evar (evk,args) when Evd.is_undefined !evdref evk ->
let ctx = evar_filtered_context (Evd.find_undefined !evdref evk) in
- let g decl a = if NamedDecl.is_local_assum decl then applyrec acc a else a in
+ let g decl a = if is_local_assum decl then applyrec acc a else a in
mkEvar (evk, Array.of_list (List.map2 g ctx (Array.to_list args)))
| _ ->
map_constr_with_binders_left_to_right
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index f9ab75cea9..29eb00c617 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -19,21 +19,21 @@ open Evarutil
open Pretype_errors
open Sigma.Notations
+module RelDecl = Context.Rel.Declaration
+
let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
let evd = Sigma.Unsafe.of_evar_map evd in
let Sigma (evk, evd, _) = new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ in
(Sigma.to_evar_map evd, evk)
let env_nf_evar sigma env =
- let open Context.Rel.Declaration in
process_rel_context
- (fun d e -> push_rel (map_constr (nf_evar sigma) d) e) env
+ (fun d e -> push_rel (RelDecl.map_constr (nf_evar sigma) d) e) env
let env_nf_betaiotaevar sigma env =
- let open Context.Rel.Declaration in
process_rel_context
(fun d e ->
- push_rel (map_constr (Reductionops.nf_betaiota sigma) d) e) env
+ push_rel (RelDecl.map_constr (Reductionops.nf_betaiota sigma) d) e) env
(****************************************)
(* Operations on value/type constraints *)
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index 4caa1e9927..1f95738621 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -16,6 +16,8 @@ open Nameops
open Termops
open Pretype_errors
+module NamedDecl = Context.Named.Declaration
+
(** Processing occurrences *)
type occurrence_error =
@@ -61,7 +63,7 @@ let proceed_with_occurrences f occs x =
let map_named_declaration_with_hyploc f hyploc acc decl =
let open Context.Named.Declaration in
- let f = f (Some (get_id decl, hyploc)) in
+ let f = f (Some (NamedDecl.get_id decl, hyploc)) in
match decl,hyploc with
| LocalAssum (id,_), InHypValueOnly ->
error_occurrences_error (IncorrectInValueOccurrence id)
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 0dd64697c6..ffb9f8940a 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -20,6 +20,8 @@ open Nativecode
open Nativevalues
open Context.Rel.Declaration
+module RelDecl = Context.Rel.Declaration
+
(** This module implements normalization by evaluation to OCaml code *)
exception Find_at of int
@@ -122,7 +124,7 @@ let build_case_type dep p realargs c =
(* TODO move this function *)
let type_of_rel env n =
- lookup_rel n env |> get_type |> lift n
+ lookup_rel n env |> RelDecl.get_type |> lift n
let type_of_prop = mkSort type1_sort
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 1ef96e0344..a172d25607 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -44,7 +44,8 @@ open Evarconv
open Pattern
open Misctypes
open Sigma.Notations
-open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
type var_map = constr_under_binders Id.Map.t
@@ -460,7 +461,7 @@ let pretype_id pretype k0 loc env evdref lvar id =
end;
(* Check if [id] is a section or goal variable *)
try
- { uj_val = mkVar id; uj_type = (get_type (lookup_named id env)) }
+ { uj_val = mkVar id; uj_type = NamedDecl.get_type (lookup_named id env) }
with Not_found ->
(* [id] not found, standard error message *)
error_var_not_found_loc loc id
@@ -505,7 +506,7 @@ let pretype_ref loc evdref env ref us =
match ref with
| VarRef id ->
(* Section variable *)
- (try make_judge (mkVar id) (get_type (lookup_named id env))
+ (try make_judge (mkVar id) (NamedDecl.get_type (lookup_named id env))
with Not_found ->
(* This may happen if env is a goal env and section variables have
been cleared - section variables should be different from goal
@@ -1043,8 +1044,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
let f decl (subst,update) =
- let id = get_id decl in
- let t = replace_vars subst (get_type decl) in
+ let id = NamedDecl.get_id decl in
+ let t = replace_vars subst (NamedDecl.get_type decl) in
let c, update =
try
let c = List.assoc id update in
@@ -1056,7 +1057,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
if is_conv env.ExtraEnv.env !evdref t t' then mkRel n, update else raise Not_found
with Not_found ->
try
- let t' = lookup_named id env |> get_type in
+ let t' = lookup_named id env |> NamedDecl.get_type in
if is_conv env.ExtraEnv.env !evdref t t' then mkVar id, update else raise Not_found
with Not_found ->
user_err_loc (loc,"",str "Cannot interpret " ++
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 98b36fb92f..5b67af3e73 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -20,6 +20,9 @@ open Termops
open Arguments_renaming
open Context.Rel.Declaration
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
type retype_error =
| NotASort
| NotAnArity
@@ -78,8 +81,7 @@ let sort_of_atomic_type env sigma ft args =
in concl_of_arity env 0 ft (Array.to_list args)
let type_of_var env id =
- let open Context.Named.Declaration in
- try get_type (lookup_named id env)
+ try NamedDecl.get_type (lookup_named id env)
with Not_found -> retype_error (BadVariable id)
let decomp_sort env sigma t =
@@ -94,7 +96,7 @@ let retype ?(polyprop=true) sigma =
(try strip_outer_cast (Evd.meta_ftype sigma n).Evd.rebus
with Not_found -> retype_error (BadMeta n))
| Rel n ->
- let ty = get_type (lookup_rel n env) in
+ let ty = RelDecl.get_type (lookup_rel n env) in
lift n ty
| Var id -> type_of_var env id
| Const cst -> rename_type_of_constant env cst
@@ -239,7 +241,7 @@ let sorts_of_context env evc ctxt =
| [] -> env,[]
| d :: ctxt ->
let env,sorts = aux ctxt in
- let s = get_sort_of env evc (get_type d) in
+ let s = get_sort_of env evc (RelDecl.get_type d) in
(push_rel d env,s::sorts) in
snd (aux ctxt)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 820a81b5d2..c1d4a34038 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -25,6 +25,9 @@ open Patternops
open Locus
open Sigma.Notations
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
(* Errors *)
type reduction_tactic_error =
@@ -54,13 +57,12 @@ let is_evaluable env = function
| EvalVarRef id -> is_evaluable_var env id
let value_of_evaluable_ref env evref u =
- let open Context.Named.Declaration in
match evref with
| EvalConstRef con ->
(try constant_value_in env (con,u)
with NotEvaluableConst IsProj ->
raise (Invalid_argument "value_of_evaluable_ref"))
- | EvalVarRef id -> lookup_named id env |> get_value |> Option.get
+ | EvalVarRef id -> lookup_named id env |> NamedDecl.get_value |> Option.get
let evaluable_of_global_reference env = function
| ConstRef cst when is_evaluable_const env cst -> EvalConstRef cst
@@ -112,22 +114,18 @@ let unsafe_reference_opt_value env sigma eval =
| Declarations.Def c -> Some (Mod_subst.force_constr c)
| _ -> None)
| EvalVar id ->
- let open Context.Named.Declaration in
- lookup_named id env |> get_value
+ lookup_named id env |> NamedDecl.get_value
| EvalRel n ->
- let open Context.Rel.Declaration in
- lookup_rel n env |> map_value (lift n) |> get_value
+ lookup_rel n env |> RelDecl.map_value (lift n) |> RelDecl.get_value
| EvalEvar ev -> Evd.existential_opt_value sigma ev
let reference_opt_value env sigma eval u =
match eval with
| EvalConst cst -> constant_opt_value_in env (cst,u)
| EvalVar id ->
- let open Context.Named.Declaration in
- lookup_named id env |> get_value
+ lookup_named id env |> NamedDecl.get_value
| EvalRel n ->
- let open Context.Rel.Declaration in
- lookup_rel n env |> map_value (lift n) |> get_value
+ lookup_rel n env |> RelDecl.map_value (lift n) |> RelDecl.get_value
| EvalEvar ev -> Evd.existential_opt_value sigma ev
exception NotEvaluable
@@ -541,11 +539,9 @@ let match_eval_ref_value env sigma constr =
| Const (sp, u) when is_evaluable env (EvalConstRef sp) ->
Some (constant_value_in env (sp, u))
| Var id when is_evaluable env (EvalVarRef id) ->
- let open Context.Named.Declaration in
- lookup_named id env |> get_value
+ lookup_named id env |> NamedDecl.get_value
| Rel n ->
- let open Context.Rel.Declaration in
- lookup_rel n env |> map_value (lift n) |> get_value
+ lookup_rel n env |> RelDecl.map_value (lift n) |> RelDecl.get_value
| Evar ev -> Evd.existential_opt_value sigma ev
| _ -> None
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 9fff64ae51..c3cdb361ba 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -17,6 +17,9 @@ open Util
open Typeclasses_errors
open Libobject
open Context.Rel.Declaration
+
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
(*i*)
let typeclasses_unique_solutions = ref false
@@ -181,7 +184,7 @@ let subst_class (subst,cl) =
let do_subst_con c = Mod_subst.subst_constant subst c
and do_subst c = Mod_subst.subst_mps subst c
and do_subst_gr gr = fst (subst_global subst gr) in
- let do_subst_ctx = List.smartmap (map_constr do_subst) in
+ let do_subst_ctx = List.smartmap (RelDecl.map_constr do_subst) in
let do_subst_context (grs,ctx) =
List.smartmap (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b)) grs,
do_subst_ctx ctx in
@@ -198,16 +201,15 @@ let discharge_class (_,cl) =
let repl = Lib.replacement_context () in
let rel_of_variable_context ctx = List.fold_right
( fun (decl,_) (ctx', subst) ->
- let open Context.Named.Declaration in
- let decl' = decl |> map_constr (substn_vars 1 subst) |> to_rel in
- (decl' :: ctx', Context.Named.Declaration.get_id decl :: subst)
+ let decl' = decl |> NamedDecl.map_constr (substn_vars 1 subst) |> NamedDecl.to_rel in
+ (decl' :: ctx', NamedDecl.get_id decl :: subst)
) ctx ([], []) in
let discharge_rel_context subst n rel =
let rel = Context.Rel.map (Cooking.expmod_constr repl) rel in
let ctx, _ =
List.fold_right
(fun decl (ctx, k) ->
- map_constr (substn_vars k subst) decl :: ctx, succ k
+ RelDecl.map_constr (substn_vars k subst) decl :: ctx, succ k
)
rel ([], n)
in ctx
@@ -220,7 +222,7 @@ let discharge_class (_,cl) =
let discharge_context ctx' subst (grs, ctx) =
let grs' =
let newgrs = List.map (fun decl ->
- match decl |> get_type |> class_of_constr with
+ match decl |> RelDecl.get_type |> class_of_constr with
| None -> None
| Some (_, ((tc,_), _)) -> Some (tc.cl_impl, true))
ctx'
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 0c1ce0d2f8..e9ee55d37c 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -29,7 +29,9 @@ open Locus
open Locusops
open Find_subterm
open Sigma.Notations
-open Context.Named.Declaration
+
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
let keyed_unification = ref (false)
let _ = Goptions.declare_bool_option {
@@ -78,9 +80,8 @@ let occur_meta_evd sigma mv c =
let abstract_scheme env evd c l lname_typ =
List.fold_left2
(fun (t,evd) (locc,a) decl ->
- let open Context.Rel.Declaration in
- let na = get_name decl in
- let ta = get_type decl in
+ let na = RelDecl.get_name decl in
+ let ta = RelDecl.get_type decl in
let na = match kind_of_term a with Var id -> Name id | _ -> na in
(* [occur_meta ta] test removed for support of eelim/ecase but consequences
are unclear...
@@ -1472,10 +1473,10 @@ let indirectly_dependent c d decls =
it is needed otherwise, as e.g. when abstracting over "2" in
"forall H:0=2, H=H:>(0=1+1) -> 0=2." where there is now obvious
way to see that the second hypothesis depends indirectly over 2 *)
- List.exists (fun d' -> dependent_in_decl (mkVar (get_id d')) d) decls
+ List.exists (fun d' -> dependent_in_decl (mkVar (NamedDecl.get_id d')) d) decls
let indirect_dependency d decls =
- decls |> List.filter (fun d' -> dependent_in_decl (mkVar (get_id d')) d) |> List.hd |> get_id
+ decls |> List.filter (fun d' -> dependent_in_decl (mkVar (NamedDecl.get_id d')) d) |> List.hd |> NamedDecl.get_id
let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) =
let current_sigma = Sigma.to_evar_map current_sigma in
@@ -1594,7 +1595,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
let likefirst = clause_with_generic_occurrences occs in
let mkvarid () = mkVar id in
let compute_dependency _ d (sign,depdecls) =
- let hyp = get_id d in
+ let hyp = NamedDecl.get_id d in
match occurrences_of_hyp hyp occs with
| NoOccurrences, InHyp ->
if indirectly_dependent c d depdecls then
@@ -1631,7 +1632,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
replace_term_occ_modulo occ test mkvarid concl
in
let lastlhyp =
- if List.is_empty depdecls then None else Some (get_id (List.last depdecls)) in
+ if List.is_empty depdecls then None else Some (NamedDecl.get_id (List.last depdecls)) in
let res = match out test with
| None -> None
| Some (sigma, c) -> Some (Sigma.Unsafe.of_pair (c, sigma))
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index c396f593bb..331ad0912f 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -17,6 +17,9 @@ open Reduction
open Vm
open Context.Rel.Declaration
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
(*******************************************)
(* Calcul de la forme normal d'un terme *)
(*******************************************)
@@ -203,12 +206,11 @@ and constr_type_of_idkey env (idkey : Vars.id_key) stk =
in
nf_univ_args ~nb_univs mk env stk
| VarKey id ->
- let open Context.Named.Declaration in
- let ty = get_type (lookup_named id env) in
+ let ty = NamedDecl.get_type (lookup_named id env) in
nf_stk env (mkVar id) ty stk
| RelKey i ->
let n = (nb_rel env - i) in
- let ty = get_type (lookup_rel n env) in
+ let ty = RelDecl.get_type (lookup_rel n env) in
nf_stk env (mkRel n) (lift n ty) stk
and nf_stk ?from:(from=0) env c t stk =
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 12:26:45 +0000