From 6899bace8e617f38fadce0b4b660d951d73af5d0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sat, 4 Feb 2017 14:47:53 +0100
Subject: Applying same convention as in Definition for parsing type in a let
 in.

---
 parsing/g_constr.ml4 | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 744d58b78..c127e7880 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -240,6 +240,9 @@ GEXTEND Gram
           mkCLambdaN (!@loc) bl c
       | "let"; id=name; bl = binders; ty = type_cstr; ":=";
         c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
+          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" ->
-- 
cgit v1.2.3