diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-18 10:51:00 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-18 10:51:00 +0000 |
| commit | e76e87e49516fab6173a29ff20099d1136c2bd49 (patch) | |
| tree | ff7165f205826e282db41c61d0275cb77430c139 | |
| parent | 141738906969de8cb9503823bc1866b0c83fc17e (diff) | |
Blindage vis a vis des constructeurs partiellement appliques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4937 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/equality.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 40f1d2255..1615d4b90 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -236,9 +236,11 @@ let find_positions env sigma t1 t2 = let hd2,args2 = whd_betadeltaiota_stack env sigma t2 in match (kind_of_term hd1, kind_of_term hd2) with - | Construct sp1, Construct sp2 -> - (* both sides are constructors, so either we descend, or we can - discriminate here. *) + | Construct sp1, Construct sp2 + when List.length args1 = mis_constructor_nargs_env env sp1 + -> + (* both sides are fully applied constructors, so either we descend, + or we can discriminate here. *) if sp1 = sp2 then List.flatten (list_map2_i |