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.
---
 pretyping/typing.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'pretyping/typing.ml')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index c4eb6af89..aaec73f04 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -29,7 +29,6 @@ let meta_type evd mv =
   let ty =
     try Evd.meta_ftype evd mv
     with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv) ++ str ".") in
-  let ty = Evd.map_fl EConstr.of_constr ty in
   meta_instance evd ty
 
 let inductive_type_knowing_parameters env sigma (ind,u) jl =
@@ -129,7 +128,7 @@ let e_is_correct_arity env evdref c pj ind specif params =
         then error ()
     | Evar (ev,_), [] ->
         let evd, s = Evd.fresh_sort_in_family env !evdref (max_sort allowed_sorts) in
-        evdref := Evd.define ev (Constr.mkSort s) evd
+        evdref := Evd.define ev (mkSort s) evd
     | _, (LocalDef _ as d)::ar' ->
         srec (push_rel d env) (lift 1 pt') ar'
     | _ ->
-- 
cgit v1.2.3