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.
---
 plugins/nsatz/nsatz.ml  | 30 +++++++++++++++---------------
 plugins/nsatz/nsatz.mli |  2 +-
 2 files changed, 16 insertions(+), 16 deletions(-)

(limited to 'plugins/nsatz')

diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml
index 72934a15d..559dfab52 100644
--- a/plugins/nsatz/nsatz.ml
+++ b/plugins/nsatz/nsatz.ml
@@ -8,7 +8,7 @@
 
 open CErrors
 open Util
-open Term
+open Constr
 open Tactics
 open Coqlib
 
@@ -204,42 +204,42 @@ else
     mkt_app ttpow [Lazy.force tz; mkt_term t1; mkt_n (num_of_int n)]
 
 let rec parse_pos p =
-  match kind_of_term p with
+  match Constr.kind p with
 | App (a,[|p2|]) ->
-    if eq_constr a (Lazy.force pxO) then num_2 */ (parse_pos p2)
+    if Constr.equal a (Lazy.force pxO) then num_2 */ (parse_pos p2)
     else num_1 +/ (num_2 */ (parse_pos p2))
 | _ -> num_1
 
 let parse_z z =
-  match kind_of_term z with
+  match Constr.kind z with
 | App (a,[|p2|]) ->
-    if eq_constr a (Lazy.force zpos) then parse_pos p2 else (num_0 -/ (parse_pos p2))
+    if Constr.equal a (Lazy.force zpos) then parse_pos p2 else (num_0 -/ (parse_pos p2))
 | _ -> num_0
 
 let parse_n z =
-  match kind_of_term z with
+  match Constr.kind z with
 | App (a,[|p2|]) ->
     parse_pos p2
 | _ -> num_0
 
 let rec parse_term p =
-  match kind_of_term p with
+  match Constr.kind p with
 | App (a,[|_;p2|]) ->
-    if eq_constr a (Lazy.force ttvar) then Var (string_of_num (parse_pos p2))
-    else if eq_constr a (Lazy.force ttconst) then Const (parse_z p2)
-    else if eq_constr a (Lazy.force ttopp) then Opp (parse_term p2)
+    if Constr.equal a (Lazy.force ttvar) then Var (string_of_num (parse_pos p2))
+    else if Constr.equal a (Lazy.force ttconst) then Const (parse_z p2)
+    else if Constr.equal a (Lazy.force ttopp) then Opp (parse_term p2)
     else Zero
 | App (a,[|_;p2;p3|]) ->
-    if eq_constr a (Lazy.force ttadd) then Add (parse_term p2, parse_term p3)
-    else if eq_constr a (Lazy.force ttsub) then Sub (parse_term p2, parse_term p3)
-    else if eq_constr a (Lazy.force ttmul) then Mul (parse_term p2, parse_term p3)
-    else if eq_constr a (Lazy.force ttpow) then
+    if Constr.equal a (Lazy.force ttadd) then Add (parse_term p2, parse_term p3)
+    else if Constr.equal a (Lazy.force ttsub) then Sub (parse_term p2, parse_term p3)
+    else if Constr.equal a (Lazy.force ttmul) then Mul (parse_term p2, parse_term p3)
+    else if Constr.equal a (Lazy.force ttpow) then
       Pow (parse_term p2, int_of_num (parse_n p3))
     else Zero
 | _ -> Zero
 
 let rec parse_request lp =
-  match kind_of_term lp with
+  match Constr.kind lp with
     | App (_,[|_|])  -> []
     | App (_,[|_;p;lp1|])  ->
 	(parse_term p)::(parse_request lp1)
diff --git a/plugins/nsatz/nsatz.mli b/plugins/nsatz/nsatz.mli
index d6e3071aa..e50a12a50 100644
--- a/plugins/nsatz/nsatz.mli
+++ b/plugins/nsatz/nsatz.mli
@@ -6,4 +6,4 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-val nsatz_compute : Term.constr -> unit Proofview.tactic
+val nsatz_compute : Constr.t -> unit Proofview.tactic
-- 
cgit v1.2.3