diff options
| author | herbelin | 2008-08-05 15:38:31 +0000 |
|---|---|---|
| committer | herbelin | 2008-08-05 15:38:31 +0000 |
| commit | 04fb64e05365cb6eaf56baeffc72aa0b5d4b9a1b (patch) | |
| tree | 26f5008ac4e4379128854cd3396c682c06792e94 /pretyping/evarconv.ml | |
| parent | 93db5abc5de50a6c43e2b94915cedce29b4a9c02 (diff) | |
Correction de bugs:
- evarconv: mauvaise idée d'utiliser la conversion sur la tête d'un
terme applicatif au moment de tester f u1 .. un = g v1 .. vn au
premier ordre : on revient sur l'algo tel qu'il était avant le
commit 11187.
- Bug #1887 (format récursif cassé à cause de la vérification des idents).
- Nouveau choix de formattage du message "Tactic Failure".
- Nettoyage vocabulaire "match context" -> "match goal" au passage.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11305 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 4d57108603..667ea458cc 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -273,11 +273,10 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = | MaybeFlexible flex1, MaybeFlexible flex2 -> let f1 i = - if l1 <> [] && l2 <> [] then - ise_list2 i (fun i -> evar_conv_x env i CONV) - (flex1::l1) (flex2::l2) + if flex1 = flex2 then + ise_list2 i (fun i -> evar_conv_x env i CONV) l1 l2 else - (i,false) + (i,false) and f2 i = (try conv_record env i (try check_conv_record appr1 appr2 |