From 37e165075d7a77b3c3e96800a92011da4506a2a8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 5 Oct 2018 12:34:42 +0200
Subject: Using smart mkLambdaCN/mkProdCN.

---
 parsing/g_constr.mlg | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'parsing/g_constr.mlg')

diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 7cb5af787b..e25f7aa54f 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -249,20 +249,20 @@ GRAMMAR EXTEND Gram
 
   record_field_declaration:
     [ [ id = global; bl = binders; ":="; c = lconstr ->
-      { (id, if bl = [] then c else mkCLambdaN ~loc bl c) } ] ]
+      { (id, mkLambdaCN ~loc bl c) } ] ]
   ;
   binder_constr:
     [ [ "forall"; bl = open_binders; ","; c = operconstr LEVEL "200" ->
-          { mkCProdN ~loc bl c }
+          { mkProdCN ~loc bl c }
       | "fun"; bl = open_binders; "=>"; c = operconstr LEVEL "200" ->
-          { mkCLambdaN ~loc bl c }
+          { mkLambdaCN ~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), { CAst.v = CCast(c, CastConv t) } -> (Loc.tag ?loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *)
           | _, _ -> ty, c1 in
-          CAst.make ~loc @@ CLetIn(id,mkCLambdaN ?loc:(constr_loc c1) bl c1,
-                 Option.map (mkCProdN ?loc:(fst ty) bl) (snd ty), c2) }
+          CAst.make ~loc @@ CLetIn(id,mkLambdaCN ?loc:(constr_loc c1) bl c1,
+                 Option.map (mkProdCN ?loc:(fst ty) bl) (snd ty), c2) }
       | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" ->
           { let fixp = mk_single_fix fx in
           let { CAst.loc = li; v = id } = match fixp.CAst.v with
-- 
cgit v1.2.3