From 03e21974a3e971a294533bffb81877dc1bd270b6 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 6 Nov 2017 23:27:09 +0100
Subject: [api] Move structures deprecated in the API to the core.

We do up to `Term` which is the main bulk of the changes.
---
 engine/evd.ml | 19 ++++++++++---------
 1 file changed, 10 insertions(+), 9 deletions(-)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index 86ab2263f..a1cb0ec68 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -8,10 +8,11 @@
 
 open Pp
 open CErrors
+open Sorts
 open Util
 open Names
 open Nameops
-open Term
+open Constr
 open Vars
 open Environ
 
@@ -126,7 +127,7 @@ end
 
 module Store = Store.Make ()
 
-type evar = Term.existential_key
+type evar = existential_key
 
 let string_of_existential evk = "?X" ^ string_of_int (Evar.repr evk)
 
@@ -242,7 +243,7 @@ let evar_instance_array test_id info args =
     instrec filter (evar_context info) 0
 
 let make_evar_instance_array info args =
-  evar_instance_array (NamedDecl.get_id %> isVarId) info args
+  evar_instance_array (NamedDecl.get_id %> Term.isVarId) info args
 
 let instantiate_evar_array info c args =
   let inst = make_evar_instance_array info args in
@@ -280,9 +281,9 @@ type 'a freelisted = {
 (* Collects all metavars appearing in a constr *)
 let metavars_of c =
   let rec collrec acc c =
-    match kind_of_term c with
+    match kind c with
       | Meta mv -> Int.Set.add mv acc
-      | _         -> Term.fold_constr collrec acc c
+      | _         -> Constr.fold collrec acc c
   in
   collrec Int.Set.empty c
 
@@ -706,10 +707,10 @@ let extract_all_conv_pbs evd =
   extract_conv_pbs evd (fun _ -> true)
 
 let loc_of_conv_pb evd (pbty,env,t1,t2) =
-  match kind_of_term (fst (decompose_app t1)) with
+  match kind (fst (Term.decompose_app t1)) with
   | Evar (evk1,_) -> fst (evar_source evk1 evd)
   | _ ->
-  match kind_of_term (fst (decompose_app t2)) with
+  match kind (fst (Term.decompose_app t2)) with
   | Evar (evk2,_) -> fst (evar_source evk2 evd)
   | _             -> None
 
@@ -720,9 +721,9 @@ let loc_of_conv_pb evd (pbty,env,t1,t2) =
 
 let evars_of_term c =
   let rec evrec acc c =
-    match kind_of_term c with
+    match kind c with
     | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l)
-    | _ -> Term.fold_constr evrec acc c
+    | _ -> Constr.fold evrec acc c
   in
   evrec Evar.Set.empty c
 
-- 
cgit v1.2.3