| Commit message (Collapse) | Author | Age |
|
|
|
|
|
| |
This is not perfect though, some primitives are unsound, and some
higher-order API should use polymorphic functions so as not to depend
on a given level.
|
| |
|
|
|
|
| |
Empirically it works better on some notations than on others and I have no idea why. I've seen notations not printing their arguments, for instance, and other printing perfectly.
|
|
|
|
|
|
|
|
|
|
|
| |
1. Proofview.Goal.enter into Proofview.Goal.nf_enter.
2. Proofview.Goal.raw_enter into Proofview.Goal.enter.
3. Proofview.Goal.goals -> Proofview.Goals.nf_goals
4. Proofview.Goal.raw_goals -> Proofview.Goals.goals
5. Ftactic.goals -> Ftactic.nf_goals
6. Ftactic.raw_goals -> Ftactic.goals
This is more uniform with the other functions of Coq.
|
|
The code for the module was moved from Tacinterp. We still expose partially
the implementation of the Ftactic.t type, for the sake of simplicity. It may
be dangerous if used improperly though.
|