From 3a0b543af4ac99b29efdebe27b1d204d044a7bf0 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sat, 31 Mar 2018 17:43:18 +0200
Subject: Evar maps contain econstrs.

We bootstrap the circular evar_map <-> econstr dependency by moving
the internal EConstr.API module to Evd.MiniEConstr. Then we make the
Evd functions use econstr.
---
 vernac/class.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'vernac/class.ml')

diff --git a/vernac/class.ml b/vernac/class.ml
index 59d933108..f0b01061b 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -181,6 +181,7 @@ let build_id_coercion idf_opt source poly =
   let sigma, vs = match source with
     | CL_CONST sp -> Evd.fresh_global env sigma (ConstRef sp)
     | _ -> error_not_transparent source in
+  let vs = EConstr.Unsafe.to_constr vs in
   let c = match constant_opt_value_in env (destConst vs) with
     | Some c -> c
     | None -> error_not_transparent source in
-- 
cgit v1.2.3