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 /pretyping/evarutil.mli | |
| 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
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 2 |
1 files changed, 1 insertions, 1 deletions
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 (***********************************************************) |