From 0cdb7e42f64674e246d4e24e3c725e23ceeec6bd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 21 Nov 2016 12:13:05 +0100
Subject: Reductionops now return EConstrs.

---
 printing/prettyp.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'printing')

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index ab0ce7e56e..e66d3aafed 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -73,7 +73,8 @@ let print_ref reduce ref =
   let typ = Global.type_of_global_unsafe ref in
   let typ =
     if reduce then
-      let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty (EConstr.of_constr typ)
+      let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty (EConstr.of_constr typ) in
+      let ccl = EConstr.Unsafe.to_constr ccl
       in it_mkProd_or_LetIn ccl ctx
     else typ in
   let univs = Global.universes_of_global ref in
@@ -595,6 +596,7 @@ let gallina_print_context with_values =
 
 let gallina_print_eval red_fun env sigma _ {uj_val=trm;uj_type=typ} =
   let ntrm = red_fun env sigma (EConstr.of_constr trm) in
+  let ntrm = EConstr.Unsafe.to_constr ntrm in
   (str "     = " ++ gallina_print_typed_value_in_env env sigma (ntrm,typ))
 
 (******************************************)
-- 
cgit v1.2.3