| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
This reverts commit 043d6a5c113a11fe9955cbe71b8f4bcd08af9a90.
|
| |
|
|
|
| |
arguments of vernac extensions, so that in list with a separator, the
separator is printed.
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
The glob_expr was actually always embedded as a VFun, so this patch should
not change anything semantically. The only change occurs in the plugin API
where one should use the Tacinterp.tactic_of_value function instead of
Tacinterp.eval_tactic.
Moreover, this patch allows to use tactics returning arguments from the ML
side.
|
| |\ |
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
Backported from trunk.
|
| | | |
|
| |\| |
|
| | | |
|
| |/
|
|
|
| |
Furthermore, ML tactic dispatch is not done according to the
type of its argument anymore.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
printing/RichPrinter: Rename into Richprinter.
printing/{ppvernac, ppconstr, pptactic}: Rename RichPp into Richpp.
printing/Richprinter: Cosmetics.
|
| |
|
|
|
|
| |
printing/Pptactic: Tag tactics pretty-printing.
printing/Ppvernac: Use the relevent Pptactic pretty-printer.
printing/RichPrinter: Publish two new services.
|
| |
|
|
| |
printing/Pptactic: Use it.
|
| |
|
|
|
|
|
|
|
|
| |
Re-add, in fact, since it was there in v8.3 but was dead code in v8.4 hence was deleted. It is necessary for printing info traces, however. A lot of the code had changed since v8.3, so adapting the code was non-trivial and some thing may be printed wrong.
It require re-adding a [tacexpr] argument to [gen_tactic_expr]. It had been made obsolete by the deletion of [pr_tactic] in v8.4 (even though printing [glob_tactic_expr] in a [tactic_expr] is only an approximation of the appropriate behaviour).
A new kind of argument, [delayed_constr], has made an appearance between v8.4 and trunk, and it differs from [constr] in the typed level. So it required its own parameter in [gen_tactic_expr]. At this point [delayed_constr] are printed in the globalised level because they are interpreted as closures. Maybe a better approximation is warranted.
Both in the printing of rewrite and induction, I changed a [pr_lconstr] (note the 'l') by a [pr_dconstr]. It is probably not quite correct, and may need fixing (adding a [pr_dlconstr] to [Pptactics] I guess?).
|
| |
|
|
| |
potentially conflicting tactics names from different plugins.
|
| | |
|
| |
|
|
| |
adding a new grammar entry for clauses
|
| |
|
|
|
|
|
|
| |
With ocaml 4.01, the 'unused open' warning also checks the mli :-)
Beware: some open are reported as useless when compiling with camlp5,
but are necessary for compatibility with camlp4. These open are now
marked with a comment.
|
| |
|
|
|
|
|
|
|
| |
Instead of putting the body directly in the AST, we register it in a table.
This time it should work properly. Tactic notation are given kernel names to
ensure the unicity of their contents.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17079 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16594 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Now, instead of having three unrelated types describing a dynamic
type at each level (raw, glob, top), we have a "('a, 'b, 'c) genarg_type"
whose parameters describe the reified type at each level.
This has various advantages:
- No more code duplication to handle the three level separately;
- Safer code: one is not authorized to mix unrelated types when what
was morally expected was a genarg_type.
- Each level-specialized representation can be accessed through
well-typed projections: rawwit, glbwit and topwit.
Documenting a bit Genarg b.t.w.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16564 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
This env argument was just there by analogy with the glob_tactic
case, and actually ignored for raw_tactic
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16301 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
This instance of gen_tactic_expr was used only to decorate
tactics via Refiner.abstract_tactics and alii, but these
expressions are now ignored by the new proof-engine (no "info"...).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15865 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
things up. Records are used instead of their equivalents as tuples.
This is maybe syntactically heavier, but this is semantically
equivalent and easier to understand.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15848 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15391 85f007b7-540e-0410-9357-904b9bb8a0f7
|
Pierre-Marie Pédrot
Hugo Herbelin
Maxime Dénès
Pierre Corbineau
Yann Régis-Gianas
Arnaud Spiwack
Julien Forest
Pierre Letouzey
ppedrot
letouzey
herbelin