diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-03-01 19:50:59 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-03-02 20:00:02 +0100 |
| commit | 4b68dbe3428740a61cda825d3a45047571d9f299 (patch) | |
| tree | 487dff0e37d819e7de07196eac6f4699f8ab1f96 /plugins/funind/g_indfun.ml4 | |
| parent | 412f848e681e3c94c635f65638310a13d675449e (diff) | |
Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code
NB: new file miscprint.ml deserves to be part of printing.cma,
but should be part of proofs.cma for the moment, due to use in logic.ml
Diffstat (limited to 'plugins/funind/g_indfun.ml4')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index ca90b3759..cc9ae912d 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -78,7 +78,8 @@ END let pr_intro_as_pat prc _ _ pat = match pat with - | Some pat -> spc () ++ str "as" ++ spc () ++ pr_intro_pattern pat + | Some pat -> + spc () ++ str "as" ++ spc () ++ Miscprint.pr_intro_pattern pat | None -> mt () |