aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml59
-rw-r--r--pretyping/evarconv.ml36
-rw-r--r--pretyping/evarsolve.ml23
-rw-r--r--pretyping/evarsolve.mli12
-rw-r--r--pretyping/recordops.ml22
-rw-r--r--pretyping/recordops.mli3
-rw-r--r--pretyping/retyping.ml12
-rw-r--r--pretyping/unification.ml15
-rw-r--r--pretyping/unification.mli2
9 files changed, 106 insertions, 78 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 5de0745d17..a793e217d4 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1784,25 +1784,24 @@ let abstract_tycon ?loc env sigma subst tycon extenv t =
!evdref, ans
let build_tycon ?loc env tycon_env s subst tycon extenv sigma t =
- let sigma, t, tt = match t with
+ let s = mkSort s in
+ match t with
| None ->
(* This is the situation we are building a return predicate and
we are in an impossible branch *)
let n = Context.Rel.length (rel_context !!env) in
let n' = Context.Rel.length (rel_context !!tycon_env) in
- let sigma, (impossible_case_type, u) =
- Evarutil.new_type_evar (reset_context !!env) ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase)
- sigma univ_flexible_alg
- in
- (sigma, lift (n'-n) impossible_case_type, mkSort u)
+ let src = Loc.tag ?loc Evar_kinds.ImpossibleCase in
+ let sigma, impossible_case_type =
+ Evarutil.new_evar (reset_context !!env) sigma ~src ~typeclass_candidate:false s in
+ (sigma, { uj_val = lift (n'-n) impossible_case_type; uj_type = s })
| Some t ->
let sigma, t = abstract_tycon ?loc tycon_env sigma subst tycon extenv t in
let sigma, tt = Typing.type_of !!extenv sigma t in
- (sigma, t, tt) in
- match unify_leq_delay !!env sigma tt (mkSort s) with
- | exception Evarconv.UnableToUnify _ -> anomaly (Pp.str "Build_tycon: should be a type.");
- | sigma ->
- sigma, { uj_val = t; uj_type = tt }
+ match unify_leq_delay !!env sigma tt s with
+ | exception Evarconv.UnableToUnify _ -> anomaly (Pp.str "Build_tycon: should be a type.");
+ | sigma -> (sigma, { uj_val = t; uj_type = tt })
+
(* For a multiple pattern-matching problem Xi on t1..tn with return
* type T, [build_inversion_problem Gamma Sigma (t1..tn) T] builds a return
@@ -1915,9 +1914,24 @@ let build_inversion_problem ~program_mode loc env sigma tms t =
it = None } } ] in
(* [pb] is the auxiliary pattern-matching serving as skeleton for the
return type of the original problem Xi *)
- let s' = Retyping.get_sort_of !!env sigma t in
- let sigma, s = Evd.new_sort_variable univ_flexible sigma in
- let sigma = Evd.set_leq_sort !!env sigma s' s in
+ let s = Retyping.get_sort_of !!env sigma t in
+ let sigma, s = Sorts.(match s with
+ | SProp | Prop | Set ->
+ (* To anticipate a possible restriction on an elimination from
+ SProp, Prop or (impredicative) Set we preserve the sort of the
+ main branch, knowing that the default impossible case shall
+ always be coercible to one of those *)
+ sigma, s
+ | Type _ ->
+ (* If the sort has algebraic universes, we cannot use this sort a
+ type constraint for the impossible case; especially if the
+ default case is not the canonical one provided in Prop by Coq
+ but one given by the user, which may be in either sort (an
+ example is in Vector.caseS', even if this one can probably be
+ put in Prop too with some care) *)
+ let sigma, s' = Evd.new_sort_variable univ_flexible sigma in
+ let sigma = Evd.set_leq_sort !!env sigma s s' in
+ sigma, s') in
let pb =
{ env = pb_env;
pred = (*ty *) mkSort s;
@@ -2066,6 +2080,15 @@ let prepare_predicate_from_arsign_tycon ~program_mode env sigma loc tomatchs ars
Some (sigma', p, arsign)
with e when precatchable_exception e -> None
+let expected_elimination_sort env tomatchl =
+ List.fold_right (fun (_,tm) s ->
+ match tm with
+ | IsInd (_,IndType(indf,_),_) ->
+ (* Not a degenerated line, see coerce_to_indtype *)
+ let s' = Inductive.elim_sort (Inductive.lookup_mind_specif env (fst (fst (dest_ind_family indf)))) in
+ if Sorts.family_leq s s' then s else s'
+ | NotInd _ -> s) tomatchl Sorts.InType
+
(* Builds the predicate. If the predicate is dependent, its context is
* made of 1+nrealargs assumptions for each matched term in an inductive
* type and 1 assumption for each term not _syntactically_ in an
@@ -2116,8 +2139,12 @@ let prepare_predicate ?loc ~program_mode typing_fun env sigma tomatchs arsign ty
| Some rtntyp ->
(* We extract the signature of the arity *)
let building_arsign,envar = List.fold_right_map (push_rel_context ~hypnaming:KeepUserNameAndRenameExistingButSectionNames sigma) arsign env in
- let sigma, newt = new_sort_variable univ_flexible sigma in
- let sigma, predcclj = typing_fun (mk_tycon (mkSort newt)) envar sigma rtntyp in
+ (* We put a type constraint on the predicate so that one
+ branch type-checked first does not lead to a lower type than
+ another branch; we take into account the possible elimination
+ constraints on the predicate *)
+ let sigma, rtnsort = fresh_sort_in_family sigma (expected_elimination_sort !!env tomatchs) in
+ let sigma, predcclj = typing_fun (Some (mkSort rtnsort)) envar sigma rtntyp in
let predccl = nf_evar sigma predcclj.uj_val in
[sigma, predccl, building_arsign]
in
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index ca16c52026..cdf2922516 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -244,24 +244,20 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
Prod (_,a,b) -> (* assert (l2=[]); *)
let _, a, b = destProd sigma t2 in
if noccurn sigma 1 b then
- lookup_canonical_conversion (proji, Prod_cs),
+ lookup_canonical_conversion env (proji, Prod_cs),
(Stack.append_app [|a;pop b|] Stack.empty)
else raise Not_found
| Sort s ->
let s = ESorts.kind sigma s in
- lookup_canonical_conversion
+ lookup_canonical_conversion env
(proji, Sort_cs (Sorts.family s)),[]
| Proj (p, c) ->
- let c2 = GlobRef.ConstRef (Projection.constant p) in
- let c = Retyping.expand_projection env sigma p c [] in
- let _, args = destApp sigma c in
- let sk2 = Stack.append_app args sk2 in
- lookup_canonical_conversion (proji, Const_cs c2), sk2
+ lookup_canonical_conversion env (proji, Proj_cs (Projection.repr p)), Stack.append_app [|c|] sk2
| _ ->
let (c2, _) = try destRef sigma t2 with DestKO -> raise Not_found in
- lookup_canonical_conversion (proji, Const_cs c2),sk2
+ lookup_canonical_conversion env (proji, Const_cs c2),sk2
with Not_found ->
- let (c, cs) = lookup_canonical_conversion (proji,Default_cs) in
+ let (c, cs) = lookup_canonical_conversion env (proji,Default_cs) in
(c,cs),[]
in
let t', { o_DEF = c; o_CTX = ctx; o_INJ=n; o_TABS = bs;
@@ -273,6 +269,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
| Some c -> (* A primitive projection applied to c *)
let ty = Retyping.get_type_of ~lax:true env sigma c in
let (i,u), ind_args =
+ (* Are we sure that ty is not an evar? *)
try Inductiveops.find_mrectype env sigma ty
with _ -> raise Not_found
in Stack.append_app_list ind_args Stack.empty, c, sk1
@@ -1317,6 +1314,7 @@ let check_selected_occs env sigma c occ occs =
raise (PretypeError (env,sigma,NoOccurrenceFound (c,None)))
else ()
+(* Error local to the module *)
exception TypingFailed of evar_map
let set_of_evctx l =
@@ -1347,12 +1345,6 @@ let thin_evars env sigma sign c =
let c' = applyrec (env,0) c in
(!sigma, c')
-exception NotFoundInstance of exn
-let () = CErrors.register_handler (function
- | NotFoundInstance e ->
- Some Pp.(str "Failed to instantiate evar: " ++ CErrors.print e)
- | _ -> None)
-
let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
try
let evi = Evd.find_undefined evd evk in
@@ -1495,9 +1487,8 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
List.exists (fun c -> isVarId evd id (EConstr.of_constr c)) l ->
instantiate_evar evar_unify flags env_rhs evd ev vid
| _ -> evd)
- with e when CErrors.noncritical e ->
- let e, info = Exninfo.capture e in
- Exninfo.iraise (NotFoundInstance e, info)
+ with IllTypedInstance _ (* from instantiate_evar *) | TypingFailed _ ->
+ user_err (Pp.str "Cannot find an instance.")
else
((if debug_ho_unification () then
let evi = Evd.find evd evk in
@@ -1626,12 +1617,15 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 =
in
Success (solve_refl ~can_drop:true f flags env evd
(position_problem true pbty) evk1 args1 args2)
- | Evar ev1, Evar ev2 when app_empty ->
+ | Evar (evk1,_ as ev1), Evar ev2 when app_empty ->
(* solve_evar_evar handles the cases ev1 and/or ev2 are frozen *)
- Success (solve_evar_evar ~force:true
+ (try
+ Success (solve_evar_evar ~force:true
(evar_define evar_unify flags ~choose:true)
evar_unify flags env evd
(position_problem true pbty) ev1 ev2)
+ with IllTypedInstance (env,t,u) ->
+ UnifFailure (evd,InstanceNotSameType (evk1,env,t,u)))
| Evar ev1,_ when is_evar_allowed flags (fst ev1) && Array.length l1 <= Array.length l2 ->
(* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *)
(* and otherwise second-order matching *)
@@ -1714,7 +1708,7 @@ let solve_unconstrained_impossible_cases env evd =
let evd' = Evd.merge_context_set Evd.univ_flexible_alg ?loc evd' ctx in
let ty = j_type j in
let flags = default_flags env in
- instantiate_evar evar_unify flags env evd' evk ty
+ instantiate_evar evar_unify flags env evd' evk ty (* should we protect from raising IllTypedInstance? *)
| _ -> evd') evd evd
let solve_unif_constraints_with_heuristics env
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 715b80f428..44414aa6a0 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -227,8 +227,7 @@ let recheck_applications unify flags env evdref t =
(match unify flags TypeUnification env !evdref Reduction.CUMUL argsty.(i) dom with
| Success evd -> evdref := evd;
aux (succ i) (subst1 args.(i) codom)
- | UnifFailure (evd, reason) ->
- Pretype_errors.error_cannot_unify env evd ~reason (argsty.(i), dom))
+ | UnifFailure (evd, reason) -> raise (IllTypedInstance (env, ty, argsty.(i))))
| _ -> raise (IllTypedInstance (env, ty, argsty.(i)))
else ()
in aux 0 fty
@@ -810,7 +809,8 @@ let check_evar_instance unify flags env evd evk1 body =
(* This happens in practice, cf MathClasses build failure on 2013-3-15 *)
let ty =
try Retyping.get_type_of ~lax:true evenv evd body
- with Retyping.RetypeError _ -> user_err (Pp.(str "Ill-typed evar instance"))
+ with Retyping.RetypeError _ ->
+ let loc, _ = evi.evar_source in user_err ?loc (Pp.(str "Ill-typed evar instance"))
in
match unify flags TypeUnification evenv evd Reduction.CUMUL ty evi.evar_concl with
| Success evd -> evd
@@ -935,13 +935,6 @@ let project_with_effects aliases sigma t subst =
in
filter_solution (Int.Map.fold is_projectable subst [])
-open Context.Named.Declaration
-let rec find_solution_type evarenv = function
- | (id,ProjectVar)::l -> get_type (lookup_named id evarenv)
- | [id,ProjectEvar _] -> (* bugged *) get_type (lookup_named id evarenv)
- | (id,ProjectEvar _)::l -> find_solution_type evarenv l
- | [] -> assert false
-
(* In case the solution to a projection problem requires the instantiation of
* subsidiary evars, [do_projection_effects] performs them; it
* also try to instantiate the type of those subsidiary evars if their
@@ -1552,10 +1545,10 @@ let rec invert_definition unify flags choose imitate_defs
raise (NotEnoughInformationToProgress sols);
(* No unique projection but still restrict to where it is possible *)
(* materializing is necessary, but is restricting useful? *)
- let ty = find_solution_type (evar_filtered_env env evi) sols in
- let ty' = instantiate_evar_array evi ty argsv in
+ let t' = of_alias t in
+ let ty = Retyping.get_type_of env !evdref t' in
let (evd,evar,(evk',argsv' as ev')) =
- materialize_evar (evar_define unify flags ~choose) env !evdref 0 ev ty' in
+ materialize_evar (evar_define unify flags ~choose) env !evdref 0 ev ty in
let ts = expansions_of_var evd aliases t in
let test c = isEvar evd c || List.exists (is_alias evd c) ts in
let filter = restrict_upon_filter evd evk test argsv' in
@@ -1564,7 +1557,7 @@ let rec invert_definition unify flags choose imitate_defs
let evd = match candidates with
| NoUpdate ->
let evd, ev'' = restrict_applied_evar evd ev' filter NoUpdate in
- add_conv_oriented_pb ~tail:false (None,env,mkEvar ev'',of_alias t) evd
+ add_conv_oriented_pb ~tail:false (None,env,mkEvar ev'',t') evd
| UpdateWith _ ->
restrict_evar evd evk' filter candidates
in
@@ -1575,7 +1568,7 @@ let rec invert_definition unify flags choose imitate_defs
match EConstr.kind !evdref t with
| Rel i when i>k ->
let open Context.Rel.Declaration in
- (match Environ.lookup_rel (i-k) env' with
+ (match Environ.lookup_rel i env' with
| LocalAssum _ -> project_variable (RelAlias (i-k))
| LocalDef (_,b,_) ->
try project_variable (RelAlias (i-k))
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 8ff2d7fc63..094dae4828 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -99,7 +99,9 @@ type conversion_check = unify_flags -> unification_kind ->
Preconditions:
- [ev] does not occur in [c].
- [c] does not contain any Meta(_)
- *)
+
+ If [ev] and [c] have non inferably convertible types, an exception
+ [IllTypedInstance] is raised *)
val instantiate_evar : unifier -> unify_flags -> env -> evar_map ->
Evar.t -> constr -> evar_map
@@ -107,7 +109,9 @@ val instantiate_evar : unifier -> unify_flags -> env -> evar_map ->
(** [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]),
possibly solving related unification problems, possibly leaving open
some problems that cannot be solved in a unique way (except if choose is
- true); fails if the instance is not valid for the given [ev] *)
+ true); fails if the instance is not valid for the given [ev];
+ If [ev] and [c] have non inferably convertible types, an exception
+ [IllTypedInstance] is raised *)
val evar_define : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool ->
env -> evar_map -> bool option -> existential -> constr -> evar_map
@@ -129,6 +133,8 @@ val solve_evar_evar : ?force:bool ->
(env -> evar_map -> bool option -> existential -> constr -> evar_map) ->
unifier -> unify_flags ->
env -> evar_map -> bool option -> existential -> existential -> evar_map
+ (** The two evars are expected to be in inferably convertible types;
+ if not, an exception IllTypedInstance is raised *)
val solve_simple_eqn : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool -> env -> evar_map ->
bool option * existential * constr -> unification_result
@@ -147,9 +153,9 @@ val noccur_evar : env -> evar_map -> Evar.t -> constr -> bool
exception IllTypedInstance of env * types * types
-(* May raise IllTypedInstance if types are not convertible *)
val check_evar_instance : unifier -> unify_flags ->
env -> evar_map -> Evar.t -> constr -> evar_map
+ (** May raise IllTypedInstance if types are not convertible *)
val remove_instance_local_defs :
evar_map -> Evar.t -> 'a list -> 'a list
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index e6e5ad8dd4..b6e44265ae 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -144,19 +144,21 @@ type obj_typ = {
type cs_pattern =
Const_cs of GlobRef.t
+ | Proj_cs of Projection.Repr.t
| Prod_cs
| Sort_cs of Sorts.family
| Default_cs
-let eq_cs_pattern p1 p2 = match p1, p2 with
-| Const_cs gr1, Const_cs gr2 -> GlobRef.equal gr1 gr2
+let eq_cs_pattern env p1 p2 = match p1, p2 with
+| Const_cs gr1, Const_cs gr2 -> Environ.QGlobRef.equal env gr1 gr2
+| Proj_cs p1, Proj_cs p2 -> Environ.QProjection.Repr.equal env p1 p2
| Prod_cs, Prod_cs -> true
| Sort_cs s1, Sort_cs s2 -> Sorts.family_equal s1 s2
| Default_cs, Default_cs -> true
| _ -> false
-let rec assoc_pat a = function
- | ((pat, t), e) :: xs -> if eq_cs_pattern pat a then (t, e) else assoc_pat a xs
+let rec assoc_pat env a = function
+ | ((pat, t), e) :: xs -> if eq_cs_pattern env pat a then (t, e) else assoc_pat env a xs
| [] -> raise Not_found
@@ -179,10 +181,7 @@ let rec cs_pattern_of_constr env t =
patt, n, args @ Array.to_list vargs
| Rel n -> Default_cs, Some n, []
| Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b]
- | Proj (p, c) ->
- let ty = Retyping.get_type_of_constr env c in
- let _, params = Inductive.find_rectype env ty in
- Const_cs (GlobRef.ConstRef (Projection.constant p)), None, params @ [c]
+ | Proj (p, c) -> Proj_cs (Projection.repr p), None, [c]
| Sort s -> Sort_cs (Sorts.family s), None, []
| _ -> Const_cs (fst @@ destRef t) , None, []
@@ -238,6 +237,7 @@ let compute_canonical_projections env ~warn (gref,ind) =
let pr_cs_pattern = function
Const_cs c -> Nametab.pr_global_env Id.Set.empty c
+ | Proj_cs p -> Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef (Projection.Repr.constant p))
| Prod_cs -> str "_ -> _"
| Default_cs -> str "_"
| Sort_cs s -> Sorts.pr_sort_family s
@@ -253,7 +253,7 @@ let register_canonical_structure ~warn env sigma o =
compute_canonical_projections env ~warn o |>
List.iter (fun ((proj, (cs_pat, _ as pat)), s) ->
let l = try GlobRef.Map.find proj !object_table with Not_found -> [] in
- match assoc_pat cs_pat l with
+ match assoc_pat env cs_pat l with
| exception Not_found ->
object_table := GlobRef.Map.add proj ((pat, s) :: l) !object_table
| _, cs ->
@@ -320,8 +320,8 @@ let check_and_decompose_canonical_structure env sigma ref =
error_not_structure ref (str "Got too few arguments to the record or structure constructor.");
(ref,indsp)
-let lookup_canonical_conversion (proj,pat) =
- assoc_pat pat (GlobRef.Map.find proj !object_table)
+let lookup_canonical_conversion env (proj,pat) =
+ assoc_pat env pat (GlobRef.Map.find proj !object_table)
let decompose_projection sigma c args =
match EConstr.kind sigma c with
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 3be60d5e62..5b8dc8184a 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -67,6 +67,7 @@ val find_primitive_projection : Constant.t -> Projection.Repr.t option
(** A cs_pattern characterizes the form of a component of canonical structure *)
type cs_pattern =
Const_cs of GlobRef.t
+ | Proj_cs of Projection.Repr.t
| Prod_cs
| Sort_cs of Sorts.family
| Default_cs
@@ -88,7 +89,7 @@ val pr_cs_pattern : cs_pattern -> Pp.t
type cs = GlobRef.t * inductive
-val lookup_canonical_conversion : (GlobRef.t * cs_pattern) -> constr * obj_typ
+val lookup_canonical_conversion : Environ.env -> (GlobRef.t * cs_pattern) -> constr * obj_typ
val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map ->
cs -> unit
val subst_canonical_structure : Mod_subst.substitution -> cs -> cs
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 4bd22e76cb..34bcd0982c 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -67,6 +67,14 @@ let get_type_from_constraints env sigma t =
| _ -> raise Not_found
else raise Not_found
+let sort_of_arity_with_constraints env sigma t =
+ try Reductionops.sort_of_arity env sigma t
+ with Reduction.NotArity ->
+ try
+ let t = get_type_from_constraints env sigma t in
+ Reductionops.sort_of_arity env sigma t
+ with Not_found | Reduction.NotArity -> retype_error NotAnArity
+
let rec subst_type env sigma typ = function
| [] -> typ
| h::rest ->
@@ -187,9 +195,7 @@ let retype ?(polyprop=true) sigma =
let mip = lookup_mind_specif env ind in
let paramtyps = Array.map_to_list (fun arg () ->
let t = type_of env arg in
- let s = try Reductionops.sort_of_arity env sigma t
- with Reduction.NotArity -> retype_error NotAnArity
- in
+ let s = sort_of_arity_with_constraints env sigma t in
Sorts.univ_of_sort (ESorts.kind sigma s))
args
in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 982814fdfc..c352a6ac1f 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -38,7 +38,7 @@ type metabinding = (metavariable * EConstr.constr * (instance_constraint * insta
type subst0 =
(evar_map *
metabinding list *
- (Environ.env * EConstr.existential * EConstr.t) list)
+ ((Environ.env * int) * EConstr.existential * EConstr.t) list)
module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
@@ -227,7 +227,7 @@ let solve_pattern_eqn_array (env,nb) f l c (sigma,metasubst,evarsubst : subst0)
| Evar ev ->
let env' = pop_rel_context nb env in
let sigma,c = pose_all_metas_as_evars env' sigma c in
- sigma,metasubst,(env,ev,solve_pattern_eqn env sigma l c)::evarsubst
+ sigma,metasubst,((env,nb),ev,solve_pattern_eqn env sigma l c)::evarsubst
| _ -> assert false
let push d (env,n) = (push_rel_assum d env,n+1)
@@ -769,21 +769,21 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
| Some sigma ->
sigma, metasubst, evarsubst
| None ->
- sigma,metasubst,((curenv,ev,cN)::evarsubst)
+ sigma,metasubst,((curenvnb,ev,cN)::evarsubst)
end
| Evar (evk,_ as ev), _
when is_evar_allowed flags evk
&& not (occur_evar sigma evk cN) ->
let cmvars = free_rels sigma cM and cnvars = free_rels sigma cN in
if Int.Set.subset cnvars cmvars then
- sigma,metasubst,((curenv,ev,cN)::evarsubst)
+ sigma,metasubst,((curenvnb,ev,cN)::evarsubst)
else error_cannot_unify_local curenv sigma (m,n,cN)
| _, Evar (evk,_ as ev)
when is_evar_allowed flags evk
&& not (occur_evar sigma evk cM) ->
let cmvars = free_rels sigma cM and cnvars = free_rels sigma cN in
if Int.Set.subset cmvars cnvars then
- sigma,metasubst,((curenv,ev,cM)::evarsubst)
+ sigma,metasubst,((curenvnb,ev,cM)::evarsubst)
else error_cannot_unify_local curenv sigma (m,n,cN)
| Sort s1, Sort s2 ->
(try
@@ -1357,7 +1357,7 @@ let w_merge env with_types flags (evd,metas,evars : subst0) =
(* Process evars *)
match evars with
- | (curenv,(evk,_ as ev),rhs)::evars' ->
+ | ((curenv,nb),(evk,_ as ev),rhs)::evars' ->
if Evd.is_defined evd evk then
let v = mkEvar ev in
let (evd,metas',evars'') =
@@ -1376,7 +1376,8 @@ let w_merge env with_types flags (evd,metas,evars : subst0) =
w_merge_rec evd' metas evars eqns
else
let evd' =
- let evd', rhs'' = pose_all_metas_as_evars curenv evd rhs' in
+ let env' = pop_rel_context nb curenv in
+ let evd', rhs'' = pose_all_metas_as_evars env' evd rhs' in
try solve_simple_evar_eqn eflags curenv evd' ev rhs''
with Retyping.RetypeError _ ->
error_cannot_unify curenv evd' (mkEvar ev,rhs'')
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 5462e09359..077597c278 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -105,7 +105,7 @@ type metabinding = (metavariable * constr * (instance_constraint * instance_typi
type subst0 =
(evar_map *
metabinding list *
- (Environ.env * existential * t) list)
+ ((Environ.env * int) * existential * t) list)
val w_merge : env -> bool -> core_unify_flags -> subst0 -> evar_map
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 21:07:06 +0000