aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-05-31 10:59:24 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-05-31 10:59:24 +0200
commitac8a84e3b4dc530b000e17b72c7e26f7a957420f (patch)
treebaf58d74b6629034cecb577eade044f29313cc4d /tactics
parent22db6304ffd45d7ae6e4a0acf909afb1ec55d02c (diff)
parent0dc79e09b2b7c369b35191191aa257451a536540 (diff)
Merge PR #6969: [api] Remove functions deprecated in 8.8
Diffstat (limited to 'tactics')
-rw-r--r--tactics/btermdn.ml2
-rw-r--r--tactics/class_tactics.ml1
-rw-r--r--tactics/contradiction.ml2
-rw-r--r--tactics/eauto.ml2
-rw-r--r--tactics/eqdecide.ml2
-rw-r--r--tactics/equality.ml1
-rw-r--r--tactics/hints.ml2
-rw-r--r--tactics/hipattern.ml2
-rw-r--r--tactics/inv.ml1
-rw-r--r--tactics/leminv.ml2
-rw-r--r--tactics/tacticals.ml2
-rw-r--r--tactics/tactics.ml4
-rw-r--r--tactics/term_dnet.ml2
13 files changed, 14 insertions, 11 deletions
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 8f50b0aa2..aca7f6c65 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -9,7 +9,7 @@
(************************************************************************)
open Util
-open Term
+open Constr
open EConstr
open Names
open Pattern
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 1ddb1a2bf..998efdd6d 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -18,6 +18,7 @@ open CErrors
open Util
open Names
open Term
+open Constr
open Termops
open EConstr
open Tacmach
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index c285f21e7..b92bc75bc 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -8,7 +8,7 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Term
+open Constr
open EConstr
open Hipattern
open Tactics
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 3df9e3f82..80d07c5c0 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -12,7 +12,7 @@ open Pp
open CErrors
open Util
open Names
-open Term
+open Constr
open Termops
open EConstr
open Proof_type
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index b0deeed17..176701d99 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -17,7 +17,7 @@
open Util
open Names
open Namegen
-open Term
+open Constr
open EConstr
open Declarations
open Tactics
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 8904cd170..f9e06391a 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -15,6 +15,7 @@ open Util
open Names
open Nameops
open Term
+open Constr
open Termops
open EConstr
open Vars
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 40cbfa5ab..e32807f4b 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -12,7 +12,7 @@ open Pp
open Util
open CErrors
open Names
-open Term
+open Constr
open Evd
open EConstr
open Vars
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index b8f1ed720..5d264058a 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -12,7 +12,7 @@ open Pp
open CErrors
open Util
open Names
-open Term
+open Constr
open Termops
open EConstr
open Inductiveops
diff --git a/tactics/inv.ml b/tactics/inv.ml
index b346ed223..28cfd57a2 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -14,6 +14,7 @@ open Util
open Names
open Term
open Termops
+open Constr
open EConstr
open Vars
open Namegen
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index a4cdc1592..f47e6b2cd 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -12,9 +12,9 @@ open Pp
open CErrors
open Util
open Names
-open Term
open Termops
open Environ
+open Constr
open EConstr
open Vars
open Namegen
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 6c7db26c7..732d06f8a 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -509,7 +509,7 @@ module New = struct
match Evd.evar_body evi with
| Evd.Evar_empty -> Some (evk,evi)
| Evd.Evar_defined c -> match Constr.kind (EConstr.Unsafe.to_constr c) with
- | Term.Evar (evk,l) -> is_undefined_up_to_restriction sigma evk
+ | Evar (evk,l) -> is_undefined_up_to_restriction sigma evk
| _ ->
(* We make the assumption that there is no way to refine an
evar remaining after typing from the initial term given to
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index bb57e2bf4..58c62af85 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1910,8 +1910,8 @@ let cast_no_check cast c =
exact_no_check (mkCast (c, cast, concl))
end
-let vm_cast_no_check c = cast_no_check Term.VMcast c
-let native_cast_no_check c = cast_no_check Term.NATIVEcast c
+let vm_cast_no_check c = cast_no_check VMcast c
+let native_cast_no_check c = cast_no_check NATIVEcast c
let exact_proof c =
let open Tacmach.New in
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 611799990..8bdcc6321 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -290,7 +290,7 @@ struct
| Const (c,u) -> Term (DRef (ConstRef c))
| Ind (i,u) -> Term (DRef (IndRef i))
| Construct (c,u)-> Term (DRef (ConstructRef c))
- | Term.Meta _ -> assert false
+ | Meta _ -> assert false
| Evar (i,_) ->
let meta =
try Evar.Map.find i !metas