diff options
| author | Pierre-Marie Pédrot | 2014-05-22 00:58:56 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-05-22 01:03:44 +0200 |
| commit | 9c927ebdd7e72bb4ae39b549f55f375d66683be5 (patch) | |
| tree | 3952c62a17e4b73986d5f2bb52034cd8ae57fa6e /printing/pptactic.ml | |
| parent | cfd8ec82784a5c893b63f3c82736eb76fe487ad7 (diff) | |
Removing useless use of metaids in tactic AST.
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 0dabe3a265..c7aff50866 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -965,7 +965,7 @@ let raw_printers = pr_or_by_notation pr_reference, pr_or_by_notation pr_reference, pr_reference, - pr_or_metaid pr_lident, + pr_lident, pr_raw_extend, pr_raw_alias, strip_prod_binders_expr, @@ -1017,7 +1017,7 @@ let () = Miscprint.pr_intro_pattern; Genprint.register_print0 Constrarg.wit_clause_dft_concl - (pr_clauses (Some true) (pr_or_metaid pr_lident)) + (pr_clauses (Some true) (pr_lident)) (pr_clauses (Some true) pr_lident) (pr_clauses (Some true) (fun id -> pr_lident (Loc.ghost,id))) ; |