| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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
|
