From 3aa07bc00899749dbd14ebb63cdc7007f233bdce Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 6 Apr 2012 22:01:59 +0000
Subject: Fixing a few bugs (see #2571) related to interpretation of multiple
 binders - fixing missing spaces in the format of the exists' notations
 (Logic.v); - fixing wrong variable name in check_is_hole error message
 (topconstr.ml); - interpret expressions with open binders such as "forall x
 y, t" as   "forall (x:_) (y:_),t" instead of "forall (x y:_),t" to avoid  
 the "implicit type" of a variable being propagated to the type of   another
 variable of different base name.

An open question remains: when writing explicitly "forall (x y:_),t",
should the types of x and y be the same or not. To avoid the "bug"
that x and y have implicit types but the one of x takes precedences, I
enforced the interpretation (in constrintern, not in parsing) that
"forall (x y:_),t" means the same as "forall (x:_) (y:_),t". However,
another choice could have been made. Then one would have to check that
if x and y have implicit types, they are the same; also, glob_constr
should ideally be changed to support a GProd and GLam with multiple
names in the same type, especially if this type is an evar. On the
contrary, one might also want e.g. "forall x y : list _, t" to mean
"forall (x:list _) (y:list _), t" with distinct instanciations of
"_" ...).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15121 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/topconstr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/topconstr.ml')

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 8db5b0afa2..7d3acf66a8 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -240,7 +240,7 @@ let compare_recursive_parts found f (iterator,subc) =
   | GLambda (_,Name x,_,t_x,c), GLambda (_,Name y,_,t_y,term)
   | GProd (_,Name x,_,t_x,c), GProd (_,Name y,_,t_y,term) ->
       (* We found a binding position where it differs *)
-      check_is_hole y t_x;
+      check_is_hole x t_x;
       check_is_hole y t_y;
       !diff = None && (diff := Some (x,y,None); aux c term)
   | _ ->
-- 
cgit v1.2.3