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 +++++-----
 vernac/comAssumption.ml |  5 ++---
 vernac/g_vernac.mlg     | 16 ++++++++--------
 3 files changed, 15 insertions(+), 16 deletions(-)

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
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 750ed35cbc..9497f2fb03 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -84,8 +84,7 @@ match local with
   in
     (gr,inst,Lib.is_modtype_strict ())
 
-let interp_assumption sigma env impls bl c =
-  let c = mkCProdN ?loc:(local_binders_loc bl) bl c in
+let interp_assumption sigma env impls c =
   let sigma, (ty, impls) = interp_type_evars_impls env sigma ~impls c in
   sigma, (ty, impls)
 
@@ -148,7 +147,7 @@ let do_assumptions kind nl l =
   in
   (* We intepret all declarations in the same evar_map, i.e. as a telescope. *)
   let (sigma,_,_),l = List.fold_left_map (fun (sigma,env,ienv) (is_coe,(idl,c)) ->
-    let sigma,(t,imps) = interp_assumption sigma env ienv [] c in
+    let sigma,(t,imps) = interp_assumption sigma env ienv c in
     let env =
       EConstr.push_named_context (List.map (fun {CAst.v=id} -> LocalAssum (id,t)) idl) env in
     let ienv = List.fold_right (fun {CAst.v=id} ienv ->
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index cf69a84b8b..895737b538 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -296,7 +296,7 @@ GRAMMAR EXTEND Gram
       { if List.exists (function CLocalPattern _ -> true | _ -> false) bl
       then
         (* FIXME: "red" will be applied to types in bl and Cast with remain *)
-        let c = mkCLambdaN ~loc bl c in
+        let c = mkLambdaCN ~loc bl c in
 	DefineBody ([], red, c, None)
       else
         (match c with
@@ -308,7 +308,7 @@ GRAMMAR EXTEND Gram
           then
             (* FIXME: "red" will be applied to types in bl and Cast with remain *)
             let c = CAst.make ~loc @@ CCast (c, CastConv t) in
-            (([],mkCLambdaN ~loc bl c), None)
+            (([],mkLambdaCN ~loc bl c), None)
           else ((bl, c), Some t)
         in
 	DefineBody (bl, red, c, tyo) }
@@ -419,16 +419,16 @@ GRAMMAR EXTEND Gram
   ;
   record_binder_body:
     [ [ l = binders; oc = of_type_with_opt_coercion;
-         t = lconstr -> { fun id -> (oc,AssumExpr (id,mkCProdN ~loc l t)) }
+         t = lconstr -> { fun id -> (oc,AssumExpr (id,mkProdCN ~loc l t)) }
       | l = binders; oc = of_type_with_opt_coercion;
          t = lconstr; ":="; b = lconstr -> { fun id ->
-	   (oc,DefExpr (id,mkCLambdaN ~loc l b,Some (mkCProdN ~loc l t))) }
+	   (oc,DefExpr (id,mkLambdaCN ~loc l b,Some (mkProdCN ~loc l t))) }
       | l = binders; ":="; b = lconstr -> { fun id ->
          match b.CAst.v with
 	 | CCast(b', (CastConv t|CastVM t|CastNative t)) ->
-	     (None,DefExpr(id,mkCLambdaN ~loc l b',Some (mkCProdN ~loc l t)))
+	     (None,DefExpr(id,mkLambdaCN ~loc l b',Some (mkProdCN ~loc l t)))
          | _ ->
-	     (None,DefExpr(id,mkCLambdaN ~loc l b,None)) } ] ]
+	     (None,DefExpr(id,mkLambdaCN ~loc l b,None)) } ] ]
   ;
   record_binder:
     [ [ id = name -> { (None,AssumExpr(id, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) }
@@ -448,9 +448,9 @@ GRAMMAR EXTEND Gram
   constructor_type:
     [[ l = binders;
       t= [ coe = of_type_with_opt_coercion; c = lconstr ->
-	            { fun l id -> (not (Option.is_empty coe),(id,mkCProdN ~loc l c)) }
+	            { fun l id -> (not (Option.is_empty coe),(id,mkProdCN ~loc l c)) }
             |  ->
-                 { fun l id -> (false,(id,mkCProdN ~loc l (CAst.make ~loc @@ CHole (None, IntroAnonymous, None)))) } ]
+                 { fun l id -> (false,(id,mkProdCN ~loc l (CAst.make ~loc @@ CHole (None, IntroAnonymous, None)))) } ]
 	 -> { t l }
      ]]
 ;
-- 
cgit v1.2.3