- Granted wish #2138 (support for local binders in syntax of Record fields).

- Add tests related to commits 12229 (bug #2117) and 12241 (bug #2139).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12242 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 106 insertions, 12 deletions

diff --git a/CHANGES b/CHANGES
index b59c61ef49..92fd6e11d0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -30,7 +30,8 @@ Vernacular commands
 
 - New command "Timeout <n> <command>." interprets a command and a timeout
   interrupts the interpretation after <n> seconds.
-- Option -R now supports binding Coq root read-only
+- Option -R now supports binding Coq root read-only.
+- New support for local binders in the syntax of Record/Structure fields.
 
 Tools
 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 5b4e9ce04a..387ee2b030 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -329,16 +329,22 @@ GEXTEND Gram
   record_field:
     [ [ bd = record_binder; ntn = decl_notation -> bd,ntn ] ]
   ;
+  record_binder_body:
+    [ [ l = binders_let; oc = of_type_with_opt_coercion; 
+         t = lconstr -> fun id -> (oc,AssumExpr (id,mkCProdN loc l t))
+      | l = binders_let; oc = of_type_with_opt_coercion;
+         t = lconstr; ":="; b = lconstr -> fun id ->
+	   (oc,DefExpr (id,mkCLambdaN loc l b,Some (mkCProdN loc l t)))
+      | l = binders_let; ":="; b = lconstr -> fun id ->
+         match b with
+	 | CCast(_,b, Rawterm.CastConv (_, t)) ->
+	     (false,DefExpr(id,mkCLambdaN loc l b,Some (mkCProdN loc l t)))
+         | _ ->
+	     (false,DefExpr(id,mkCLambdaN loc l b,None)) ] ]
+  ;
   record_binder:
     [ [ id = name -> (false,AssumExpr(id,CHole (loc, None)))
-      | id = name; oc = of_type_with_opt_coercion; t = lconstr ->
-         (oc,AssumExpr (id,t))
-      | id = name; oc = of_type_with_opt_coercion;
-             t = lconstr; ":="; b = lconstr -> (oc,DefExpr (id,b,Some t))
-      | id = name; ":="; b = lconstr ->
-         match b with
-             CCast(_,b, Rawterm.CastConv (_, t)) -> (false,DefExpr(id,b,Some t))
-           | _ -> (false,DefExpr(id,b,None)) ] ]
+      | id = name; f = record_binder_body -> f id ] ]
   ;
   assum_list:
     [ [ bl = LIST1 assum_coe -> bl | b = simple_assum_coe -> [b] ] ]
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index f00e5f0a1d..cf88256bcd 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -350,10 +350,10 @@ let pr_record (sp,tyi) =
       str ": " ++ pr_lconstr_env envpar arity ++ brk(1,2) ++ 
       str ":= " ++ pr_id cstrnames.(0)) ++ 
     brk(1,2) ++
-    hv 2 (str "{" ++
-      prlist_with_sep (fun () -> str ";" ++ brk(1,0))
+    hv 2 (str "{ " ++
+      prlist_with_sep (fun () -> str ";" ++ brk(2,0))
         (fun (id,b,c) -> 
-	  str " " ++ pr_id id ++ str (if b then " : " else " := ") ++ 
+	  pr_id id ++ str (if b then " : " else " := ") ++ 
 	  pr_lconstr_env envpar c) fields) ++ str" }")
 
 let gallina_print_inductive sp =
diff --git a/test-suite/bugs/closed/shouldsucceed/2117.v b/test-suite/bugs/closed/shouldsucceed/2117.v
new file mode 100644
index 0000000000..763d85e2ca
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2117.v
@@ -0,0 +1,56 @@
+(* Check pattern-unification on evars in apply unification *)
+
+Axiom app : forall tau tau':Type, (tau -> tau') -> tau -> tau'.
+
+Axiom copy : forall tau:Type, tau -> tau -> Prop.
+Axiom copyr : forall tau:Type, tau -> tau -> Prop.
+Axiom copyf : forall tau:Type, tau -> tau -> Prop.
+Axiom eq : forall tau:Type, tau -> tau -> Prop.
+Axiom subst : forall tau tau':Type, (tau -> tau') -> tau -> tau' -> Prop.
+
+Axiom copy_atom : forall tau:Type, forall t t':tau, eq tau t t' -> copy tau t t'.
+Axiom copy_fun: forall tau tau':Type, forall t t':(tau->tau'),
+(forall x:tau, copyr tau x x->copy tau' (t x) (t' x))
+->copy (tau->tau') t t'.
+
+Axiom copyr_atom : forall tau:Type, forall t t':tau, copyr tau t t' -> eq tau t t'.
+Axiom copyr_fun: forall tau tau':Type, forall t t':(tau->tau'),
+copyr (tau->tau') t t'
+->(forall x y:tau, copy tau x y->copyr tau' (t x) (t' y)).
+
+Axiom copyf_atom : forall tau:Type, forall t t':tau, copyf tau t t' -> eq tau t t'.
+Axiom copyf_fun: forall tau tau':Type, forall t t':(tau->tau'),
+copyr (tau->tau') t t'
+->(forall x y:tau, forall z1 z2:tau',
+(copy tau x y)->
+(subst tau tau' t x z1)->
+(subst tau tau' t' y z2)->
+copyf tau' z1 z2).
+
+Axiom eqappg: forall tau tau':Type, forall t:tau->tau', forall q:tau, forall r:tau',forall t':tau',
+( ((subst tau tau' t q t') /\ (eq tau' t' r))
+->eq tau' (app tau tau' t q) r).
+
+Axiom eqappd: forall tau tau':Type, forall t:tau->tau', forall q:tau, forall r:tau',
+forall t':tau', ((subst tau tau' t q t') /\ (eq tau' r t'))
+->eq tau' r (app tau tau' t q).
+
+Axiom substcopy: forall tau tau':Type, forall t:tau->tau', forall q:tau, forall r:tau',
+(forall x:tau, (copyf tau x q) -> (copy tau' (t x) r))
+->subst tau tau' t q r.
+
+Ltac EtaLong := (apply copy_fun;intros;EtaLong)|| apply copy_atom.

+Ltac Subst := apply substcopy;intros;EtaLong.
+Ltac Rigid_aux := fun A => apply A|| Rigid_aux (copyr_fun _ _ _ _ A).
+Ltac Rigid := fun A => apply copyr_atom; Rigid_aux A.
+
+Theorem church0: forall i:Type, exists X:(i->i)->i->i, 
+copy ((i->i)->i->i) (fun f:i->i => fun x:i=>f (X f x)) (fun f:i->i=>fun x:i=>app i i (X f) (f x)).
+intros.
+esplit.
+EtaLong.
+eapply eqappd;split.
+Subst.
+apply copyf_atom.
+Show Existentials.
+apply H1.
diff --git a/test-suite/bugs/closed/shouldsucceed/2139.v b/test-suite/bugs/closed/shouldsucceed/2139.v
new file mode 100644
index 0000000000..4f71d097ff
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2139.v
@@ -0,0 +1,24 @@
+(* Call of apply on <-> failed because of evars in elimination predicate *)
+
+Class Patch (patch : Type) := {
+    commute : patch -> patch -> Prop
+}.  
+    
+Parameter flip : forall	`{patchInstance	: Patch	patch}
+                       	 {a b : patch},	
+                 commute a b <-> commute b a.
+                 
+Lemma Foo : forall `{patchInstance : Patch patch}
+                    {a b : patch}, 
+            (commute a b)
+         -> True.
+Proof.   
+intros.  
+apply flip in H. 
+
+(* failed in well-formed arity check because elimination predicate of
+   iff in (@flip _ _ _ _) had normalized evars while the ones in the
+   type of (@flip _ _ _ _) itself had non-normalized evars *)
+
+(* By the way, is the check necessary ? *)
+
diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v
index 885fff4836..c0065809db 100644
--- a/test-suite/success/Record.v
+++ b/test-suite/success/Record.v
@@ -80,3 +80,10 @@ Record DecidableOrder : Type :=
 ; le_trans : transitive _ le
 ; le_total : forall x y, {x <= y}+{y <= x}
 }.
+
+(* Test syntactic sugar suggested by wish report #2138 *)
+
+Record R : Type := {
+  P (A : Type) : Prop := exists x : A -> A, x = x;
+  Q A : P A -> P A
+}.