From 0cdb7e42f64674e246d4e24e3c725e23ceeec6bd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Mon, 21 Nov 2016 12:13:05 +0100
Subject: Reductionops now return EConstrs.

---
 pretyping/vnorm.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/vnorm.mli')

diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli
index 650f3f291..8a4202c88 100644
--- a/pretyping/vnorm.mli
+++ b/pretyping/vnorm.mli
@@ -10,4 +10,4 @@ open EConstr
 open Environ
 
 (** {6 Reduction functions } *)
-val cbv_vm : env -> Evd.evar_map -> constr -> types -> Constr.t
+val cbv_vm : env -> Evd.evar_map -> constr -> types -> constr
-- 
cgit v1.2.3