From 03e21974a3e971a294533bffb81877dc1bd270b6 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
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/micromega/coq_micromega.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'plugins/micromega')

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index fc6781b067..218342efe4 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -20,6 +20,7 @@ open Pp
 open Mutils
 open Goptions
 open Names
+open Constr
 
 (**
   * Debug flag 
@@ -580,9 +581,9 @@ struct
     | Ukn
     | BadStr of string
     | BadNum of int
-    | BadTerm of Term.constr
+    | BadTerm of constr
     | Msg   of string
-    | Goal of (Term.constr list ) * Term.constr * parse_error
+    | Goal of (constr list ) * constr * parse_error
 
   let string_of_error = function
    | Ukn -> "ukn"
@@ -1521,7 +1522,7 @@ let rec witness prover   l1 l2 =
 let rec apply_ids t ids =
  match ids with
   | [] -> t
-  | i::ids -> apply_ids (Term.mkApp(t,[| Term.mkVar i |])) ids
+  | i::ids -> apply_ids (mkApp(t,[| mkVar i |])) ids
 
 let coq_Node = 
  lazy (gen_constant_in_modules "VarMap"
-- 
cgit v1.2.3