From 8f5d447769a41cd251701272a6ff71a7a20de658 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 5 Dec 2016 11:36:12 +0100
Subject: Improving the API of constrexpr_ops.mli.

Deprecating abstract_constr_expr in favor of mkCLambdaN,
prod_constr_expr in favor of mkCProdN.

Note: They did not do exactly the same, the first ones were
interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second ones
were preserving the original sharing of the type, what I think is the
correct thing to do.

So, there is also a "fix" of semantic here.
---
 vernac/command.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/command.ml')

diff --git a/vernac/command.ml b/vernac/command.ml
index 4b4f4d2711..62a5b97151 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -262,7 +262,7 @@ match local with
     (gr,inst,Lib.is_modtype_strict ())
 
 let interp_assumption evdref env impls bl c =
-  let c = prod_constr_expr c bl in
+  let c = mkCProdN (local_binders_loc bl) bl c in
   interp_type_evars_impls env evdref ~impls c
 
 let declare_assumptions idl is_coe k (c,ctx) pl imps impl_is_on nl =
-- 
cgit v1.2.3