The Coq mailing list

[Pierre Casteran <casteran AT labri.u-bordeaux.fr>]

Hello,

  In some cases, Intro forces a delta-reduction when the goal is not a
product.

  But this is not always the case with the variant of Intros where you
specify both
the number and names of variables :



 Goal (P,Q:Prop)~P -> (Q->P) ->~Q.
 Intros P Q H H0 q.   (* Fails cause (not Q) is not a product *)
 Intros P Q H H0; Intro q. (* Succeeds *)

 
Then Intros id1 ... idN can no more described as equivalent to Intro i1;
Intro i2; ... ; Intro iN.


Pierre
P.S.
  I didn't swirtch on 7.2 yet : (i'm still working with 7.1)




-- 
Pierre Casteran,
LaBRI, Universite Bordeaux-I      |   
351 Cours de la Liberation        |   
F-33405 TALENCE Cedex             |   
France                            |   
tel : (+ 33) 5 56 84 69 31
fax : (+ 33) 5 56 84 66 69
email: Pierre . Casteran @ labri . u-bordeaux . fr  (but whithout white
space)
www: http://dept-info.labri.u-bordeaux.fr/~casteran