diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-04-06 22:01:59 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-04-06 22:01:59 +0000 |
commit | 3aa07bc00899749dbd14ebb63cdc7007f233bdce (patch) | |
tree | 87183b0e2880a101a76d9cced966ff8be43dd32d /theories/Init/Logic.v | |
parent | f252d2985b2adba8ca7c309297eba4337fd83010 (diff) |
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
Diffstat (limited to 'theories/Init/Logic.v')
-rw-r--r-- | theories/Init/Logic.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index d8a028cfb..ca7d0073e 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -240,7 +240,7 @@ Definition all (A:Type) (P:A -> Prop) := forall x:A, P x. Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..)) (at level 200, x binder, right associativity, - format "'[' 'exists' '/ ' x .. y , '/ ' p ']'") + format "'[' 'exists' '/ ' x .. y , '/ ' p ']'") : type_scope. Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q)) @@ -423,7 +423,7 @@ Definition uniqueness (A:Type) (P:A->Prop) := forall x y, P x -> P y -> x = y. Notation "'exists' ! x .. y , p" := (ex (unique (fun x => .. (ex (unique (fun y => p))) ..))) (at level 200, x binder, right associativity, - format "'[' 'exists' ! '/ ' x .. y , '/ ' p ']'") + format "'[' 'exists' ! '/ ' x .. y , '/ ' p ']'") : type_scope. Lemma unique_existence : forall (A:Type) (P:A->Prop), |