Using smart mkLambdaCN/mkProdCN.

2 files changed, 10 insertions, 11 deletions

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 }
      ]]
 ;