diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-10 16:40:47 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-10 16:40:47 +0100 |
| commit | 956b7c4304582b1e9e3ca0bb34944bcbac18c0cc (patch) | |
| tree | b6c8bfaf58e1e4ad3397ff8136142001d433cdd9 /printing | |
| parent | a340265c9f88df990649481c8ecbe8a513ac4756 (diff) | |
| parent | 9360af713794cb9ecf3c5e7d686c6f486a65df7f (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstrsig.mli | 2 | ||||
| -rw-r--r-- | printing/pptactic.mli | 3 | ||||
| -rw-r--r-- | printing/pptacticsig.mli | 1 | ||||
| -rw-r--r-- | printing/printer.ml | 1 | ||||
| -rw-r--r-- | printing/richprinter.ml | 7 | ||||
| -rw-r--r-- | printing/richprinter.mli | 4 |
6 files changed, 4 insertions, 14 deletions
diff --git a/printing/ppconstrsig.mli b/printing/ppconstrsig.mli index 15413d515..b7eb9b1ff 100644 --- a/printing/ppconstrsig.mli +++ b/printing/ppconstrsig.mli @@ -12,8 +12,6 @@ open Libnames open Constrexpr open Names open Misctypes -open Locus -open Genredexpr module type Pp = sig diff --git a/printing/pptactic.mli b/printing/pptactic.mli index 50cc4e2bc..42b4c976a 100644 --- a/printing/pptactic.mli +++ b/printing/pptactic.mli @@ -15,9 +15,6 @@ open Names open Constrexpr open Tacexpr open Ppextend -open Environ -open Pattern -open Misctypes type 'a raw_extra_genarg_printer = (constr_expr -> std_ppcmds) -> diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli index ee1669f7f..1631bda37 100644 --- a/printing/pptacticsig.mli +++ b/printing/pptacticsig.mli @@ -8,7 +8,6 @@ open Pp open Genarg -open Names open Constrexpr open Tacexpr open Ppextend diff --git a/printing/printer.ml b/printing/printer.ml index 8a2d6e7bd..fb98f6073 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -11,7 +11,6 @@ open Errors open Util open Names open Term -open Vars open Environ open Globnames open Nametab diff --git a/printing/richprinter.ml b/printing/richprinter.ml index d71dc82d5..d95e19074 100644 --- a/printing/richprinter.ml +++ b/printing/richprinter.ml @@ -5,21 +5,20 @@ module RichppVernac = Ppvernac.Richpp module RichppTactic = Pptactic.Richpp type rich_pp = - string - * Ppannotation.t Richpp.located Xml_datatype.gxml + Ppannotation.t Richpp.located Xml_datatype.gxml * Xml_datatype.xml let get_annotations obj = Pp.Tag.prj obj Ppannotation.tag let make_richpp pr ast = - let raw_pp, rich_pp = + let rich_pp = rich_pp get_annotations (pr ast) in let xml = Ppannotation.( xml_of_rich_pp tag_of_annotation attributes_of_annotation rich_pp ) in - (raw_pp, rich_pp, xml) + (rich_pp, xml) let richpp_vernac = make_richpp RichppVernac.pr_vernac let richpp_constr = make_richpp RichppConstr.pr_constr_expr diff --git a/printing/richprinter.mli b/printing/richprinter.mli index c67d52c08..41c313514 100644 --- a/printing/richprinter.mli +++ b/printing/richprinter.mli @@ -20,12 +20,10 @@ (** A rich pretty-print is composed of: *) type rich_pp = - (** - a raw pretty-print ; *) - string (** - a generalized semi-structured document whose attributes are annotations ; *) - * Ppannotation.t Richpp.located Xml_datatype.gxml + Ppannotation.t Richpp.located Xml_datatype.gxml (** - an XML document, representing annotations as usual textual XML attributes. *) |