From 4401b9cb757d2b1326fbd2c3fea33013ccf08a98 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 5 Oct 2018 12:25:16 +0200
Subject: Documenting constr_expr constructors; adding smart CLam/CProd.

---
 interp/constrexpr_ops.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'interp/constrexpr_ops.ml')

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 23d0536df8..d5f0b7bff6 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -526,6 +526,14 @@ let mkAppC (f,l) =
   | CApp (g,l') -> CAst.make @@ CApp (g, l' @ l)
   | _           -> CAst.make @@ CApp ((None, f), l)
 
+let mkProdCN ?loc bll c =
+  if bll = [] then c else
+  CAst.make ?loc @@ CProdN (bll,c)
+
+let mkLambdaCN ?loc bll c =
+  if bll = [] then c else
+  CAst.make ?loc @@ CLambdaN (bll,c)
+
 let mkCProdN ?loc bll c =
   CAst.make ?loc @@ CProdN (bll,c)
 
-- 
cgit v1.2.3