diff options
-rw-r--r-- | pretyping/evarconv.ml | 8 | ||||
-rw-r--r-- | pretyping/evarutil.ml | 5 | ||||
-rw-r--r-- | pretyping/evarutil.mli | 2 |
3 files changed, 8 insertions, 7 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 6799671d1..9af633b0a 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -231,7 +231,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = | Flexible ev1, MaybeFlexible flex2 -> let f1 i = if - is_unification_pattern l1 & + is_unification_pattern ev1 l1 & not (occur_evar (fst ev1) (applist (term2,l2))) then (* Miller-Pfenning's patterns unification *) @@ -261,7 +261,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = | MaybeFlexible flex1, Flexible ev2 -> let f1 i = if - is_unification_pattern l2 & + is_unification_pattern ev2 l2 & not (occur_evar (fst ev2) (applist (term1,l1))) then (* Miller-Pfenning's patterns unification *) @@ -318,7 +318,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = | Flexible ev1, Rigid _ -> if - is_unification_pattern l1 & + is_unification_pattern ev1 l1 & not (occur_evar (fst ev1) (applist (term2,l2))) then (* Miller-Pfenning's patterns unification *) @@ -344,7 +344,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = | Rigid _, Flexible ev2 -> if - is_unification_pattern l2 & + is_unification_pattern ev2 l2 & not (occur_evar (fst ev2) (applist (term1,l1))) then (* Miller-Pfenning's patterns unification *) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index f803fd9d7..c4c5ec922 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -493,8 +493,9 @@ let head_evar = that we don't care whether args itself contains Rel's or even Rel's distinct from the ones in l *) -let is_unification_pattern l = - List.for_all isRel l & list_uniquize l = l +let is_unification_pattern (_,args) l = + let l' = Array.to_list args @ l in + List.for_all (fun a -> isRel a or isVar a) l' & list_uniquize l' = l' (* From a unification problem "?X l1 = term1 l2" such that l1 is made of distinct rel's, build "\x1...xn.(term1 l2)" (patterns unification) *) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 2aceece0b..5519b57c9 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -82,7 +82,7 @@ val define_evar_as_arrow : evar_defs -> existential -> evar_defs * types val define_evar_as_lambda : evar_defs -> existential -> evar_defs * types val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts -val is_unification_pattern : constr list -> bool +val is_unification_pattern : existential -> constr list -> bool val solve_pattern_eqn : env -> constr list -> constr -> constr (***********************************************************) |