diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-23 18:50:31 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-24 10:21:49 +0100 |
| commit | 60f6d46c6e623a39fc66a21cbac5aaecdf4c67c6 (patch) | |
| tree | 3f8f5508672a1b5ce62975ba81673d7fc2c7f6da /intf | |
| parent | 7fb5a9c518f30298a7a9332f0280c2ca0e690f18 (diff) | |
Getting rid of the "<:tactic< ... >>" quotations.
It used to allow to represent parts of tactic AST directly in ML code. Most of
the uses were trivial, only calling a constant, except for tauto that had an
important code base written in this style. Removing this reduces the dependency
to CAMLPX and the preeminence of Ltac in ML code.
Diffstat (limited to 'intf')
0 files changed, 0 insertions, 0 deletions