summaryrefslogtreecommitdiff
path: root/pretyping/unification.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/unification.ml')
-rw-r--r--pretyping/unification.ml31
1 files changed, 18 insertions, 13 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 981a5605..fb29196c 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: unification.ml 11819 2009-01-20 20:04:50Z herbelin $ *)
+(* $Id: unification.ml 11897 2009-02-09 19:28:02Z barras $ *)
open Pp
open Util
@@ -268,21 +268,25 @@ let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n =
| Some true ->
(match expand_key curenv cf1 with
| Some c ->
- unirec_rec curenvnb pb b substn (whd_betaiotazeta (mkApp(c,l1))) cN
+ unirec_rec curenvnb pb b substn
+ (whd_betaiotazeta sigma (mkApp(c,l1))) cN
| None ->
(match expand_key curenv cf2 with
| Some c ->
- unirec_rec curenvnb pb b substn cM (whd_betaiotazeta (mkApp(c,l2)))
+ unirec_rec curenvnb pb b substn cM
+ (whd_betaiotazeta sigma (mkApp(c,l2)))
| None ->
error_cannot_unify curenv sigma (cM,cN)))
| Some false ->
(match expand_key curenv cf2 with
| Some c ->
- unirec_rec curenvnb pb b substn cM (whd_betaiotazeta (mkApp(c,l2)))
+ unirec_rec curenvnb pb b substn cM
+ (whd_betaiotazeta sigma (mkApp(c,l2)))
| None ->
(match expand_key curenv cf1 with
| Some c ->
- unirec_rec curenvnb pb b substn (whd_betaiotazeta (mkApp(c,l1))) cN
+ unirec_rec curenvnb pb b substn
+ (whd_betaiotazeta sigma (mkApp(c,l1))) cN
| None ->
error_cannot_unify curenv sigma (cM,cN)))
else
@@ -489,7 +493,7 @@ let unify_to_type env evd flags c u =
let sigma = evars_of evd in
let c = refresh_universes c in
let t = get_type_of_with_meta env sigma (metas_of evd) c in
- let t = Tacred.hnf_constr env sigma (nf_betaiota (nf_meta evd t)) in
+ let t = Tacred.hnf_constr env sigma (nf_betaiota sigma (nf_meta evd t)) in
let u = Tacred.hnf_constr env sigma u in
try unify_0 env sigma Cumul flags t u
with e when precatchable_exception e -> ([],[])
@@ -613,11 +617,12 @@ let w_unify_meta_types env ?(flags=default_unify_flags) evd =
types of metavars are unifiable with the types of their instances *)
let check_types env evd flags subst m n =
- if isEvar (fst (whd_stack m)) or isEvar (fst (whd_stack n)) then
+ let sigma = evars_of evd in
+ if isEvar (fst (whd_stack sigma m)) or isEvar (fst (whd_stack sigma n)) then
unify_0_with_initial_metas subst true env (evars_of evd) topconv
flags
- (Retyping.get_type_of_with_meta env (evars_of evd) (metas_of evd) m)
- (Retyping.get_type_of_with_meta env (evars_of evd) (metas_of evd) n)
+ (Retyping.get_type_of_with_meta env sigma (metas_of evd) m)
+ (Retyping.get_type_of_with_meta env sigma (metas_of evd) n)
else
subst
@@ -738,8 +743,8 @@ let secondOrderAbstraction env flags allow_K typ (p, oplist) evd =
w_merge env false flags ([p,pred,(ConvUpToEta 0,TypeProcessed)],[]) evd'
let w_unify2 env flags allow_K cv_pb ty1 ty2 evd =
- let c1, oplist1 = whd_stack ty1 in
- let c2, oplist2 = whd_stack ty2 in
+ let c1, oplist1 = whd_stack (evars_of evd) ty1 in
+ let c2, oplist2 = whd_stack (evars_of evd) ty2 in
match kind_of_term c1, kind_of_term c2 with
| Meta p1, _ ->
(* Find the predicate *)
@@ -777,8 +782,8 @@ let w_unify2 env flags allow_K cv_pb ty1 ty2 evd =
Meta(1) had meta-variables in it. *)
let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
let cv_pb = of_conv_pb cv_pb in
- let hd1,l1 = whd_stack ty1 in
- let hd2,l2 = whd_stack ty2 in
+ let hd1,l1 = whd_stack (evars_of evd) ty1 in
+ let hd2,l2 = whd_stack (evars_of evd) ty2 in
match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with
(* Pattern case *)
| (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true)