From 118d24281bc62bb7ff503abee56f156545eb9eea Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 10 Mar 2018 23:54:14 +0100
Subject: [api] Remove deprecated object from `Term`

We remove most of what was deprecated in `Term`. Now, `intf` and
`kernel` are almost deprecation-free, tho I am not very convinced
about the whole `Term -> Constr` renaming but I'm afraid there is no
way back.

Inconsistencies with the constructor policy (see #6440) remain along
the code-base and I'm afraid I don't see a plan to reconcile them.

The `Sorts` deprecation is hard to finalize, opening `Sorts` is not a
good idea as someone added a `List` module inside it.
---
 plugins/romega/refl_omega.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'plugins/romega')

diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index d182497840..e603480656 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -8,6 +8,7 @@
 
 open Pp
 open Util
+open Constr
 open Const_omega
 module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint)
 open OmegaSolver
@@ -1036,13 +1037,13 @@ let resolution unsafe sigma env (reified_concl,reified_hyps) systems_list =
   let decompose_tactic = decompose_tree env context solution_tree in
 
   Tactics.generalize (l_generalize_arg @ l_reified_hypnames) >>
-  Tactics.convert_concl_no_check reified Term.DEFAULTcast >>
+  Tactics.convert_concl_no_check reified DEFAULTcast >>
   Tactics.apply (app coq_do_omega [|decompose_tactic|]) >>
   show_goal >>
   (if unsafe then
      (* Trust the produced term. Faster, but might fail later at Qed.
         Also handy when debugging, e.g. via a Show Proof after romega. *)
-     Tactics.convert_concl_no_check (Lazy.force coq_True) Term.VMcast
+     Tactics.convert_concl_no_check (Lazy.force coq_True) VMcast
    else
      Tactics.normalise_vm_in_concl) >>
   Tactics.apply (Lazy.force coq_I)
-- 
cgit v1.2.3