aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/inv.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/inv.ml')
-rw-r--r--tactics/inv.ml5
1 files changed, 2 insertions, 3 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml
index c5aa74ba5..8648dfb90 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -10,7 +10,6 @@ open Pp
open CErrors
open Util
open Names
-open Nameops
open Term
open Termops
open EConstr
@@ -78,7 +77,7 @@ let make_inv_predicate env evd indf realargs id status concl =
| Dep dflt_concl ->
if not (occur_var env !evd id concl) then
user_err ~hdr:"make_inv_predicate"
- (str "Current goal does not depend on " ++ pr_id id ++ str".");
+ (str "Current goal does not depend on " ++ Id.print id ++ str".");
(* We abstract the conclusion of goal with respect to
realargs and c to * be concl in order to rewrite and have
c also rewritten when the case * will be done *)
@@ -442,7 +441,7 @@ let raw_inversion inv_kind id status names =
let (ind, t) =
try pf_apply Tacred.reduce_to_atomic_ind gl (pf_unsafe_type_of gl c)
with UserError _ ->
- let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in
+ let msg = str "The type of " ++ Id.print id ++ str " is not inductive." in
CErrors.user_err msg
in
let IndType (indf,realargs) = find_rectype env sigma t in