From c8c8ccdaaffefdbd3d78c844552a08bcb7b4f915 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 26 Nov 2016 02:12:40 +0100
Subject: Evar-normalizing functions now act on EConstrs.

---
 engine/evarutil.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'engine/evarutil.mli')

diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index ea9599c8b2..67de18abce 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -139,8 +139,8 @@ val judge_of_new_Type : 'r Sigma.t -> (unsafe_judgment, 'r) Sigma.sigma
 (** [flush_and_check_evars] raise [Uninstantiated_evar] if an evar remains
     uninstantiated; [nf_evar] leaves uninstantiated evars as is *)
 
-val whd_evar :  evar_map -> constr -> constr
-val nf_evar :  evar_map -> constr -> constr
+val whd_evar :  evar_map -> EConstr.constr -> EConstr.constr
+val nf_evar :  evar_map -> EConstr.constr -> EConstr.constr
 val j_nf_evar :  evar_map -> EConstr.unsafe_judgment -> EConstr.unsafe_judgment
 val jl_nf_evar :
    evar_map -> EConstr.unsafe_judgment list -> EConstr.unsafe_judgment list
-- 
cgit v1.2.3