diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/cic.dtd | 2 | ||||
| -rw-r--r-- | dev/top_printers.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/dev/doc/cic.dtd b/dev/doc/cic.dtd index f2314e224f..cc33efd483 100644 --- a/dev/doc/cic.dtd +++ b/dev/doc/cic.dtd @@ -125,7 +125,7 @@ id ID #REQUIRED sort %sort; #REQUIRED> -<!-- The substitutions are ordered by increasing DeBrujin --> +<!-- The substitutions are ordered by increasing de Bruijn --> <!-- index. An empty substitution means that that index is --> <!-- not accessible. --> <!ELEMENT META (substitution*)> diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 474cc85c17..7caaf2d9d5 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -7,6 +7,7 @@ (************************************************************************) (* Printers for the ocaml toplevel. *) +[@@@ocaml.warning "-32"] open Util open Pp @@ -502,7 +503,6 @@ VERNAC COMMAND EXTEND PrintConstr END *) -open Pcoq open Genarg open Stdarg open Egramml |