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.
---
 plugins/ltac/extratactics.ml4 | 2 --
 plugins/ltac/rewrite.ml       | 8 ++++----
 2 files changed, 4 insertions(+), 6 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 2e90ce90c..a5f8060ae 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -296,7 +296,6 @@ let project_hint ~poly pri l2r r =
   let env = Global.env() in
   let sigma = Evd.from_env env in
   let sigma, c = Evd.fresh_global env sigma gr in
-  let c = EConstr.of_constr c in
   let t = Retyping.get_type_of env sigma c in
   let t =
     Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) t in
@@ -307,7 +306,6 @@ let project_hint ~poly pri l2r r =
   let p =
     if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in
   let sigma, p = Evd.fresh_global env sigma p in
-  let p = EConstr.of_constr p in
   let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in
   let c = it_mkLambda_or_LetIn
     (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index d32a2faef..9eb55aa5e 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -428,7 +428,8 @@ let split_head = function
   | [] -> assert(false)
 
 let eq_pb (ty, env, x, y as pb) (ty', env', x', y' as pb') =
-  pb == pb' || (ty == ty' && Constr.equal x x' && Constr.equal y y')
+  let equal x y = Constr.equal (EConstr.Unsafe.to_constr x) (EConstr.Unsafe.to_constr y) in
+  pb == pb' || (ty == ty' && equal x x' && equal y y')
 
 let problem_inclusion x y =
   List.for_all (fun pb -> List.exists (fun pb' -> eq_pb pb pb') y) x
@@ -626,9 +627,9 @@ let solve_remaining_by env sigma holes by =
         (** Evar should not be defined, but just in case *)
       | Some evi ->
         let env = Environ.reset_with_named_context evi.evar_hyps env in
-        let ty = EConstr.of_constr evi.evar_concl in
+        let ty = evi.evar_concl in
         let c, sigma = Pfedit.refine_by_tactic env sigma ty solve_tac in
-        Evd.define evk c sigma
+        Evd.define evk (EConstr.of_constr c) sigma
     in
     List.fold_left solve sigma indep
 
@@ -1862,7 +1863,6 @@ let declare_projection n instance_id r =
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let sigma,c = Evd.fresh_global env sigma r in
-  let c = EConstr.of_constr c in
   let ty = Retyping.get_type_of env sigma c in
   let term = proper_projection sigma c ty in
   let sigma, typ = Typing.type_of env sigma term in
-- 
cgit v1.2.3