diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-02-04 14:47:53 +0100 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-24 12:22:21 +0100 |
| commit | 6899bace8e617f38fadce0b4b660d951d73af5d0 (patch) | |
| tree | ed55d3abcb239da96efcb1744acb0fa457d2d777 | |
| parent | b496309c7d4707a4377c72b0543faa025d993589 (diff) | |
Applying same convention as in Definition for parsing type in a let in.
| -rw-r--r-- | parsing/g_constr.ml4 | 3 |
1 files changed, 3 insertions, 0 deletions
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" -> |