diff options
author | 2012-03-02 22:30:29 +0000 | |
---|---|---|
committer | 2012-03-02 22:30:29 +0000 | |
commit | 401f17afa2e9cc3f2d734aef0d71a2c363838ebd (patch) | |
tree | 7a3e0ce211585d4c09a182aad1358dfae0fb38ef /plugins/funind/recdef.ml | |
parent | 15cb1aace0460e614e8af1269d874dfc296687b0 (diff) |
Noise for nothing
Util only depends on Ocaml stdlib and Utf8 tables.
Generic pretty printing and loc functions are in Pp.
Generic errors are in Errors.
+ Training white-spaces, useless open, prlist copies random erasure.
Too many "open Errors" on the contrary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/funind/recdef.ml')
-rw-r--r-- | plugins/funind/recdef.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 5e0aac4c2..c37de6e4a 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -17,6 +17,7 @@ open Pp open Names open Libnames open Nameops +open Errors open Util open Closure open RedFlags @@ -1273,7 +1274,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ let sign = initialize_named_context_for_proof () in let na = next_global_ident_away name [] in if Termops.occur_existential gls_type then - Util.error "\"abstract\" cannot handle existentials"; + Errors.error "\"abstract\" cannot handle existentials"; let hook _ _ = let opacity = let na_ref = Libnames.Ident (dummy_loc,na) in @@ -1553,7 +1554,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num hook with e -> begin - ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); + ignore(try Vernacentries.vernac_reset_name (Pp.dummy_loc,functional_id) with _ -> ()); (* anomaly "Cannot create termination Lemma" *) raise e end |