diff options
| author | Pierre-Marie Pédrot | 2016-03-06 23:00:58 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-06 23:06:12 +0100 |
| commit | ffac73b8f3f3bf6877ce652eecac7849b7c2a182 (patch) | |
| tree | c309ce25302e1851fc5442ee95b7d4f36589d6ef /intf | |
| parent | cdc91f02f98b4d857bfebe61d95b920787a8d0e5 (diff) | |
Moving Autorewrite to Hightatctic.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 7273b92b9a..5501ca7c7f 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -69,7 +69,6 @@ type printable = | PrintHint of reference or_by_notation | PrintHintGoal | PrintHintDbName of string - | PrintRewriteHintDbName of string | PrintHintDb | PrintScopes | PrintScope of string |