Merge PR #6098: [api] Move structures deprecated in the API to the core.

6 files changed, 16 insertions, 16 deletions

diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 65c186a41..4b1555e55 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -415,7 +415,7 @@ VERNAC COMMAND EXTEND DeriveInversionClear
   -> [ add_inversion_lemma_exn na c s false inv_clear_tac ]
 
 | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => [ seff na ]
-  -> [ add_inversion_lemma_exn na c InProp false inv_clear_tac ]
+  -> [ add_inversion_lemma_exn na c Sorts.InProp false inv_clear_tac ]
 END
 
 VERNAC COMMAND EXTEND DeriveInversion
@@ -424,7 +424,7 @@ VERNAC COMMAND EXTEND DeriveInversion
   -> [ add_inversion_lemma_exn na c s false inv_tac ]
 
 | [ "Derive" "Inversion" ident(na) "with" constr(c) ] => [ seff na ]
-  -> [ add_inversion_lemma_exn na c InProp false inv_tac ]
+  -> [ add_inversion_lemma_exn na c Sorts.InProp false inv_tac ]
 END
 
 VERNAC COMMAND EXTEND DeriveDependentInversion
@@ -514,7 +514,7 @@ let cache_transitivity_lemma (_,(left,lem)) =
 
 let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref)
 
-let inTransitivity : bool * Term.constr -> obj =
+let inTransitivity : bool * Constr.t -> obj =
   declare_object {(default_object "TRANSITIVITY-STEPS") with
     cache_function = cache_transitivity_lemma;
     open_function = (fun i o -> if Int.equal i 1 then cache_transitivity_lemma o);
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index 104977aef..ed2d9da63 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -91,7 +91,7 @@ END
 
 (** TODO: DEPRECATE *)
 (* A progress test that allows to see if the evars have changed *)
-open Term
+open Constr
 open Proofview.Notations
 
 let rec eq_constr_mod_evars sigma x y =
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 28a13fb40..38460c669 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1120,10 +1120,10 @@ let pr_goal_selector ~toplevel s =
     let ty = EConstr.Unsafe.to_constr ty in
     let rec strip_ty acc n ty =
       if n=0 then (List.rev acc, EConstr.of_constr ty) else
-        match Term.kind_of_term ty with
-            Term.Prod(na,a,b) ->
-              strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b
-          | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
+        match Constr.kind ty with
+        | Constr.Prod(na,a,b) ->
+          strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b
+        | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
     strip_ty [] n ty
 
   let pr_atomic_tactic_level env sigma n t =
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 1809f0fcd..705a51edd 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -12,7 +12,7 @@ open CErrors
 open Util
 open Nameops
 open Namegen
-open Term
+open Constr
 open EConstr
 open Vars
 open Reduction
@@ -426,7 +426,7 @@ 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' && Term.eq_constr x x' && Term.eq_constr y y')
+  pb == pb' || (ty == ty' && Constr.equal x x' && Constr.equal y y')
 
 let problem_inclusion x y =
   List.for_all (fun pb -> List.exists (fun pb' -> eq_pb pb pb') y) x
@@ -928,8 +928,8 @@ let fold_match ?(force=false) env sigma c =
 	it_mkProd_or_LetIn (subst1 mkProp body) (List.tl ctx)
     in
     let sk = 
-      if sortp == InProp then
-	if sortc == InProp then
+      if sortp == Sorts.InProp then
+	if sortc == Sorts.InProp then
 	  if dep then case_dep_scheme_kind_from_prop
 	  else case_scheme_kind_from_prop
 	else (
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 63e891b45..1306c590b 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -37,7 +37,7 @@ type ('constr,'redexpr) strategy_ast =
 
 type rewrite_proof = 
   | RewPrf of constr * constr
-  | RewCast of Term.cast_kind
+  | RewCast of Constr.cast_kind
 
 type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *)
 
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 4d171ecbc..c03a86732 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -8,7 +8,7 @@
 
 open Util
 open Names
-open Term
+open Constr
 open EConstr
 open Misctypes
 open Genarg
@@ -172,8 +172,8 @@ let id_of_name = function
        | Sort s ->
 	  begin
 	    match ESorts.kind sigma s with
-	    | Prop _ -> Label.to_id (Label.make "Prop")
-	    | Type _ -> Label.to_id (Label.make "Type")
+	    | Sorts.Prop _ -> Label.to_id (Label.make "Prop")
+	    | Sorts.Type _ -> Label.to_id (Label.make "Type")
 	  end
        | _ -> fail()