diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-08-29 17:00:14 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-08-29 17:00:14 +0000 |
| commit | f4b250cac72454356728916fe3f8757822c26485 (patch) | |
| tree | b6c1ba3be96980b26704293d3ed0a92abd6d12ed | |
| parent | 1f7689b7c932950777fdea44f5d3f1d03abef22f (diff) | |
Prise en compte de l'instance des evars dans la détection des 'motifs'
d'unification à la Miller. Ceci devrait garantir la généralité de la
solution modulo le problème résiduel de éta : en l'absence d'éta dans
le CCI, le choix entre deux instances éta-convertibles distinctes
d'une evar, conduira à des solutions non convertibles pour le CCI.
Par exemple, le problème suivant, pour c et Q rigides, a deux
solutions distinctes non convertibles.
"fun (H: forall P:A->Prop, ~ c (fun x => P x)) (K: c (fun x => Q x)) => H _ K"
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9096 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 (***********************************************************) |