diff options
| author | pboutill | 2012-03-02 22:30:29 +0000 |
|---|---|---|
| committer | pboutill | 2012-03-02 22:30:29 +0000 |
| commit | 401f17afa2e9cc3f2d734aef0d71a2c363838ebd (patch) | |
| tree | 7a3e0ce211585d4c09a182aad1358dfae0fb38ef /plugins/firstorder | |
| 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/firstorder')
| -rw-r--r-- | plugins/firstorder/formula.ml | 1 | ||||
| -rw-r--r-- | plugins/firstorder/g_ground.ml4 | 2 | ||||
| -rw-r--r-- | plugins/firstorder/instances.ml | 2 | ||||
| -rw-r--r-- | plugins/firstorder/rules.ml | 1 | ||||
| -rw-r--r-- | plugins/firstorder/sequent.ml | 3 | ||||
| -rw-r--r-- | plugins/firstorder/sequent.mli | 1 | ||||
| -rw-r--r-- | plugins/firstorder/unify.ml | 1 |
7 files changed, 9 insertions, 2 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index d67dceeac6..566b2b8b08 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -12,6 +12,7 @@ open Term open Termops open Reductionops open Tacmach +open Errors open Util open Declarations open Libnames diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 4a38c48dcf..f5b16e43fe 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -17,7 +17,6 @@ open Tacticals open Tacinterp open Term open Names -open Util open Libnames (* declaring search depth as a global option *) @@ -103,6 +102,7 @@ let normalize_evaluables= unfold_in_hyp (Lazy.force defined_connectives) (Tacexpr.InHypType id)) *) +open Pp open Genarg open Ppconstr open Printer diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 16831d3ecc..8d4b0eee1c 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -10,6 +10,8 @@ open Formula open Sequent open Unify open Rules +open Pp +open Errors open Util open Term open Glob_term diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 23eeb2f662..b56fe4e509 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Term diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index f75678c60f..780e3f3e7e 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -7,6 +7,7 @@ (************************************************************************) open Term +open Errors open Util open Formula open Unify @@ -235,7 +236,7 @@ let print_cmap map= let print_entry c l s= let xc=Constrextern.extern_constr false (Global.env ()) c in str "| " ++ - Util.prlist Printer.pr_global l ++ + prlist Printer.pr_global l ++ str " : " ++ Ppconstr.pr_constr_expr xc ++ cut () ++ diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index c5c2bb9541..5587e9fbb5 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -7,6 +7,7 @@ (************************************************************************) open Term +open Errors open Util open Formula open Tacmach diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index 299a0054a2..48c402cc0f 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Formula open Tacmach |