diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-09 15:51:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-09 15:51:05 +0200 |
| commit | 8efb78da7900e7f13105aac8361272477f8f5119 (patch) | |
| tree | 6efe7fbf8c847b6e17239aebb7283ff125024def /printing | |
| parent | 3c481b2ef7e7abd813fdac22b4bbe8d89de88141 (diff) | |
| parent | 5ea2539d4a7d12938787a74a12112e76aaf2a4ee (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/pptactic.ml | 3 | ||||
| -rw-r--r-- | printing/pptacticsig.mli | 2 |
2 files changed, 3 insertions, 2 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 3d1e3e054..5356cdee8 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -366,7 +366,6 @@ module Make in str "<" ++ name ++ str ">" ++ args - let pr_alias_key key = try let prods = (KNmap.find key !prnotation_tab).pptac_prods in @@ -383,7 +382,7 @@ module Make str (String.concat " " (pr prods)) with Not_found -> KerName.print key - + let pr_alias_gen pr_gen lev key l = try let pp = KNmap.find key !prnotation_tab in diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli index f02785a55..c08d6044d 100644 --- a/printing/pptacticsig.mli +++ b/printing/pptacticsig.mli @@ -50,6 +50,8 @@ module type Pp = sig val pr_alias : (Val.t -> std_ppcmds) -> int -> Names.KerName.t -> Val.t list -> std_ppcmds + val pr_alias_key : Names.KerName.t -> std_ppcmds + val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds val pr_raw_tactic : raw_tactic_expr -> std_ppcmds |