diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/cc/ccproof.ml | 1 | ||||
| -rw-r--r-- | plugins/decl_mode/ppdecl_proof.ml | 1 | ||||
| -rw-r--r-- | plugins/funind/glob_termops.ml | 1 | ||||
| -rw-r--r-- | plugins/syntax/nat_syntax.ml | 2 | ||||
| -rw-r--r-- | plugins/syntax/z_syntax.ml | 1 |
5 files changed, 6 insertions, 0 deletions
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index 25c01f2bd..d5eab32c4 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -10,6 +10,7 @@ (* proof-trees that will be transformed into proof-terms in cctac.ml4 *) open Errors +open Util open Names open Term open Ccalgo diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml index 01f32e4a3..b72476a75 100644 --- a/plugins/decl_mode/ppdecl_proof.ml +++ b/plugins/decl_mode/ppdecl_proof.ml @@ -7,6 +7,7 @@ (************************************************************************) open Errors +open Util open Pp open Decl_expr open Names diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 44ae42090..f678b898b 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -1,6 +1,7 @@ open Pp open Glob_term open Errors +open Util open Names open Decl_kinds open Misctypes diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index 8f34ec495..5219124cd 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -9,11 +9,13 @@ (* This file defines the printer for natural numbers in [nat] *) (*i*) +open Util open Glob_term open Bigint open Coqlib open Pp open Errors +open Util (*i*) (**********************************************************************) diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index 7cad42d60..8e5a07e0d 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -8,6 +8,7 @@ open Pp open Errors +open Util open Names open Bigint |