diff options
Diffstat (limited to 'pretyping/find_subterm.ml')
-rw-r--r-- | pretyping/find_subterm.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index 9e7652da6..fd6bfe0a2 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -12,7 +12,6 @@ open CErrors open Names open Locus open EConstr -open Nameops open Termops open Pretype_errors @@ -30,7 +29,7 @@ let explain_invalid_occurrence l = ++ prlist_with_sep spc int l ++ str "." let explain_incorrect_in_value_occurrence id = - pr_id id ++ str " has no value." + Id.print id ++ str " has no value." let explain_occurrence_error = function | InvalidOccurrence l -> explain_invalid_occurrence l |