From a42795cc1c2a8ed3efa9960af920ff7b16d928f0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 1 Sep 2016 17:52:44 +0200
Subject: Introducing a new EConstr.t type to perform the nf_evar operation on
 demand.

---
 engine/engine.mllib | 1 +
 1 file changed, 1 insertion(+)

(limited to 'engine/engine.mllib')

diff --git a/engine/engine.mllib b/engine/engine.mllib
index 53cbbd73ef..c78f37a850 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -4,6 +4,7 @@ Universes
 UState
 Evd
 Sigma
+EConstr
 Termops
 Proofview_monad
 Evarutil
-- 
cgit v1.2.3


From be51c33a6bf91a00fdd5f3638ddb5b3cc3a2c626 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 30 Nov 2016 00:41:31 +0100
Subject: Namegen primitives now apply on evar constrs.

Incidentally, this fixes a printing bug in output/inference.v where the
displayed name of an evar was the wrong one because its type was not
evar-expanded enough.
---
 engine/engine.mllib | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/engine.mllib')

diff --git a/engine/engine.mllib b/engine/engine.mllib
index c78f37a850..1b670d3667 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -1,10 +1,10 @@
 Logic_monad
-Namegen
 Universes
 UState
 Evd
 Sigma
 EConstr
+Namegen
 Termops
 Proofview_monad
 Evarutil
-- 
cgit v1.2.3