From 3a0b543af4ac99b29efdebe27b1d204d044a7bf0 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
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.
---
 pretyping/cases.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/cases.ml')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index b16f1a9ed5..4c87b4e7ed 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1015,7 +1015,7 @@ let adjust_impossible_cases pb pred tomatch submat =
     | Evar (evk,_) when snd (evar_source evk !(pb.evdref)) == Evar_kinds.ImpossibleCase ->
         if not (Evd.is_defined !(pb.evdref) evk) then begin
 	  let evd, default = use_unit_judge !(pb.evdref) in
-	  pb.evdref := Evd.define evk (EConstr.Unsafe.to_constr default.uj_type) evd
+          pb.evdref := Evd.define evk default.uj_type evd
         end;
         add_assert_false_case pb tomatch
     | _ ->
-- 
cgit v1.2.3