From e76e87e49516fab6173a29ff20099d1136c2bd49 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 18 Nov 2003 10:51:00 +0000 Subject: 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 --- tactics/equality.ml | 8 +++++--- 1 file 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 -- cgit v1.2.3