Merge PR#417: No cast surgery in let in

4 files changed, 38 insertions, 35 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 07e4ddf84..496b20002 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -233,11 +233,11 @@ type (_, _) entry =
 | TTName : ('self, Name.t Loc.located) entry
 | TTReference : ('self, reference) entry
 | TTBigint : ('self, Bigint.bigint) entry
-| TTBinder : ('self, local_binder list) entry
+| TTBinder : ('self, local_binder_expr list) entry
 | TTConstr : prod_info * 'r target -> ('r, 'r) entry
 | TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry
-| TTBinderListT : ('self, local_binder list) entry
-| TTBinderListF : Tok.t list -> ('self, local_binder list list) entry
+| TTBinderListT : ('self, local_binder_expr list) entry
+| TTBinderListF : Tok.t list -> ('self, local_binder_expr list list) entry
 
 type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry
 
@@ -324,7 +324,7 @@ let cases_pattern_expr_of_name (loc,na) = match na with
 type 'r env = {
   constrs : 'r list;
   constrlists : 'r list list;
-  binders : (local_binder list * bool) list;
+  binders : (local_binder_expr list * bool) list;
 }
 
 let push_constr subst v = { subst with constrs = v :: subst.constrs }
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 47455f984..c127e7880 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -38,7 +38,7 @@ let mk_cast = function
     in CCast(loc, c, CastConv ty)
 
 let binder_of_name expl (loc,na) =
-  LocalRawAssum ([loc, na], Default expl,
+  CLocalAssum ([loc, na], Default expl,
     CHole (loc, Some (Evar_kinds.BinderType na), IntroAnonymous, None))
 
 let binders_of_names l =
@@ -240,17 +240,18 @@ GEXTEND Gram
           mkCLambdaN (!@loc) bl c
       | "let"; id=name; bl = binders; ty = type_cstr; ":=";
         c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
-          let loc1 =
-	    Loc.merge (local_binders_loc bl) (constr_loc c1)
-	  in
-          CLetIn(!@loc,id,mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2)
+          let ty,c1 = match ty, c1 with
+          | (_,None), CCast(loc,c, CastConv t) -> (constr_loc t,Some t), c (* Tolerance, see G_vernac.def_body *)
+          | _, _ -> ty, c1 in
+          CLetIn(!@loc,id,mkCLambdaN (constr_loc c1) bl c1,
+                 Option.map (mkCProdN (fst ty) bl) (snd ty), c2)
       | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" ->
           let fixp = mk_single_fix fx in
           let (li,id) = match fixp with
               CFix(_,id,_) -> id
             | CCoFix(_,id,_) -> id
             | _ -> assert false in
-          CLetIn(!@loc,(li,Name id),fixp,c)
+          CLetIn(!@loc,(li,Name id),fixp,None,c)
       | "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> l | "()" -> []];
 	  po = return_type;
 	  ":="; c1 = operconstr LEVEL "200"; "in";
@@ -412,11 +413,11 @@ GEXTEND Gram
   impl_ident_tail:
     [ [ "}" -> binder_of_name Implicit
     | nal=LIST1 name; ":"; c=lconstr; "}" ->
-        (fun na -> LocalRawAssum (na::nal,Default Implicit,c))
+        (fun na -> CLocalAssum (na::nal,Default Implicit,c))
     | nal=LIST1 name; "}" ->
-        (fun na -> LocalRawAssum (na::nal,Default Implicit,CHole (Loc.join_loc (fst na) !@loc, Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None)))
+        (fun na -> CLocalAssum (na::nal,Default Implicit,CHole (Loc.join_loc (fst na) !@loc, Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None)))
     | ":"; c=lconstr; "}" ->
-	(fun na -> LocalRawAssum ([na],Default Implicit,c))
+	(fun na -> CLocalAssum ([na],Default Implicit,c))
     ] ]
   ;
   fixannot:
@@ -442,12 +443,12 @@ GEXTEND Gram
        the latter is unique *)
     [ [ (* open binder *)
         id = name; idl = LIST0 name; ":"; c = lconstr ->
-          [LocalRawAssum (id::idl,Default Explicit,c)]
+          [CLocalAssum (id::idl,Default Explicit,c)]
 	(* binders factorized with open binder *)
       | id = name; idl = LIST0 name; bl = binders ->
           binders_of_names (id::idl) @ bl
       | id1 = name; ".."; id2 = name ->
-          [LocalRawAssum ([id1;(!@loc,Name ldots_var);id2],
+          [CLocalAssum ([id1;(!@loc,Name ldots_var);id2],
 	                  Default Explicit,CHole (!@loc, None, IntroAnonymous, None))]
       | bl = closed_binder; bl' = binders ->
 	  bl@bl'
@@ -457,37 +458,39 @@ GEXTEND Gram
     [ [ l = LIST0 binder -> List.flatten l ] ]
   ;
   binder:
-    [ [ id = name -> [LocalRawAssum ([id],Default Explicit,CHole (!@loc, None, IntroAnonymous, None))]
+    [ [ id = name -> [CLocalAssum ([id],Default Explicit,CHole (!@loc, None, IntroAnonymous, None))]
       | bl = closed_binder -> bl ] ]
   ;
   closed_binder:
     [ [ "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" ->
-          [LocalRawAssum (id::idl,Default Explicit,c)]
+          [CLocalAssum (id::idl,Default Explicit,c)]
       | "("; id=name; ":"; c=lconstr; ")" ->
-          [LocalRawAssum ([id],Default Explicit,c)]
+          [CLocalAssum ([id],Default Explicit,c)]
       | "("; id=name; ":="; c=lconstr; ")" ->
-          [LocalRawDef (id,c)]
+          (match c with
+          | CCast(_,c, CastConv t) -> [CLocalDef (id,c,Some t)]
+          | _ -> [CLocalDef (id,c,None)])
       | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
-          [LocalRawDef (id,CCast (Loc.merge (constr_loc t) (!@loc),c, CastConv t))]
+          [CLocalDef (id,c,Some t)]
       | "{"; id=name; "}" ->
-          [LocalRawAssum ([id],Default Implicit,CHole (!@loc, None, IntroAnonymous, None))]
+          [CLocalAssum ([id],Default Implicit,CHole (!@loc, None, IntroAnonymous, None))]
       | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" ->
-          [LocalRawAssum (id::idl,Default Implicit,c)]
+          [CLocalAssum (id::idl,Default Implicit,c)]
       | "{"; id=name; ":"; c=lconstr; "}" ->
-          [LocalRawAssum ([id],Default Implicit,c)]
+          [CLocalAssum ([id],Default Implicit,c)]
       | "{"; id=name; idl=LIST1 name; "}" ->
-          List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (!@loc, None, IntroAnonymous, None))) (id::idl)
+          List.map (fun id -> CLocalAssum ([id],Default Implicit,CHole (!@loc, None, IntroAnonymous, None))) (id::idl)
       | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" ->
-	  List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc
+	  List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Explicit, b), t)) tc
       | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" ->
-	  List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc
+	  List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Implicit, b), t)) tc
       | "'"; p = pattern LEVEL "0" ->
           let (p, ty) =
             match p with
             | CPatCast (_, p, ty) -> (p, Some ty)
             | _ -> (p, None)
           in
-          [LocalPattern (!@loc, p, ty)]
+          [CLocalPattern (!@loc, p, ty)]
     ] ]
   ;
   typeclass_constraint:
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 23f1dccaf..ded7a557c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -243,7 +243,7 @@ GEXTEND Gram
         | _ -> DefineBody (bl, red, c, None))
     | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
         let ((bl, c), tyo) =
-          if List.exists (function LocalPattern _ -> true | _ -> false) bl
+          if List.exists (function CLocalPattern _ -> true | _ -> false) bl
           then
             let c = CCast (!@loc, c, CastConv t) in
             (expand_pattern_binders mkCLambdaN bl c, None)
@@ -334,8 +334,8 @@ GEXTEND Gram
   binder_nodef:
     [ [ b = binder_let ->
       (match b with
-          LocalRawAssum(l,ty) -> (l,ty)
-        | LocalRawDef _ ->
+          CLocalAssum(l,ty) -> (l,ty)
+        | CLocalDef _ ->
             Util.user_err_loc
               (loc,"fix_param",Pp.str"defined binder not allowed here.")) ] ]
   ;
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index cf5174af9..6c148d393 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -162,11 +162,11 @@ module Constr :
     val pattern : cases_pattern_expr Gram.entry
     val constr_pattern : constr_expr Gram.entry
     val lconstr_pattern : constr_expr Gram.entry
-    val closed_binder : local_binder list Gram.entry
-    val binder : local_binder list Gram.entry (* closed_binder or variable *)
-    val binders : local_binder list Gram.entry (* list of binder *)
-    val open_binders : local_binder list Gram.entry
-    val binders_fixannot : (local_binder list * (Id.t located option * recursion_order_expr)) Gram.entry
+    val closed_binder : local_binder_expr list Gram.entry
+    val binder : local_binder_expr list Gram.entry (* closed_binder or variable *)
+    val binders : local_binder_expr list Gram.entry (* list of binder *)
+    val open_binders : local_binder_expr list Gram.entry
+    val binders_fixannot : (local_binder_expr list * (Id.t located option * recursion_order_expr)) Gram.entry
     val typeclass_constraint : (Name.t located * bool * constr_expr) Gram.entry
     val record_declaration : constr_expr Gram.entry
     val appl_arg : (constr_expr * explicitation located option) Gram.entry