index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
printing
Commit message (
Expand
)
Author
Age
*
Add a interpreted level [tacexpr] to [Tacexpr] together with its printer.
Arnaud Spiwack
2014-11-01
*
Info: print a name for the primitive tactics in [Proofview].
Arnaud Spiwack
2014-11-01
*
Add [Info] command.
Arnaud Spiwack
2014-11-01
*
This commit introduces changes in induction and destruct.
Hugo Herbelin
2014-10-25
*
Pushing Pierre's factorization of names in goal context printing from
Hugo Herbelin
2014-10-22
*
Experimental printing of the signature of open evars in Check.
Hugo Herbelin
2014-10-17
*
Goal: remove most of the API (make [Goal.goal] concrete).
Arnaud Spiwack
2014-10-16
*
Emit a warning for void Arguments statement (Close 3713)
Enrico Tassi
2014-10-13
*
library/opaqueTables: enable their use in interactive mode
Enrico Tassi
2014-10-13
*
Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name
Matthieu Sozeau
2014-10-11
*
Removing Convert_concl and Convert_hyp from Logic.
Hugo Herbelin
2014-10-09
*
Going back on granting wish #1039 in f5d7b2b1e so that apply with
Hugo Herbelin
2014-10-01
*
Seeing IntroWildcard as an action intro pattern rather than as a naming pattern
Hugo Herbelin
2014-09-30
*
Add syntax for naming new goals in refine: writing ?[id] instead of _
Hugo Herbelin
2014-09-30
*
Notation: option to attach extra pretty printing rules to notations
Enrico Tassi
2014-09-29
*
Printing evar instance in a more intuitive order.
Hugo Herbelin
2014-09-29
*
Fix printing of primitive record info.
Matthieu Sozeau
2014-09-29
*
Print information about primitive records (Print and About).
Matthieu Sozeau
2014-09-28
*
Improve consistency of whitespace (beautifier).
Xavier Clerc
2014-09-25
*
Using an or_var rather than the hack with loc for coding a pure ident
Hugo Herbelin
2014-09-24
*
Fix a message.
Arnaud Spiwack
2014-09-24
*
coqtop -emacs: do not declare "still unfocused goals" as an "infomsg".
Arnaud Spiwack
2014-09-24
*
Fix debug printing with primitive projections.
Matthieu Sozeau
2014-09-18
*
Revert specific syntax for primitive projections, avoiding ugly
Matthieu Sozeau
2014-09-17
*
Add a "Hint Mode ref (+ | -)*" hint for setting a global mode
Matthieu Sozeau
2014-09-15
*
Not printing goal name (reinstalled by mistake in a previous commit).
Hugo Herbelin
2014-09-15
*
Fixing bug #3619 in emacs mode.
Hugo Herbelin
2014-09-15
*
Prepare goal name printing but no not print them at the current time.
Hugo Herbelin
2014-09-13
*
Checking typability of evar instances. Using ";" to separate bindings
Hugo Herbelin
2014-09-13
*
Add syntax [id]: to apply tactic to goal named id.
Hugo Herbelin
2014-09-12
*
Use evar name to print goal.
Hugo Herbelin
2014-09-12
*
Parsing evar instances.
Hugo Herbelin
2014-09-12
*
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-09-12
*
Replace the list of argument in tacexpr with a single row argument.
Arnaud Spiwack
2014-09-12
*
VernacExtend does not dispatch on type anymore.
Pierre-Marie Pédrot
2014-09-10
*
Removing the XML plugin.
Pierre-Marie Pédrot
2014-09-08
*
Parsing of Type@{max(i,j)}.
Matthieu Sozeau
2014-09-08
*
Removing the old implementation of clear_body.
Pierre-Marie Pédrot
2014-09-05
*
Revert the two previous commits. I was testing in the wrong branch.
Pierre-Marie Pédrot
2014-09-04
*
Removing the old implementation of clear_body.
Pierre-Marie Pédrot
2014-09-04
*
Remove [Infer] option of records.
Arnaud Spiwack
2014-09-04
*
Inductive and CoInductive records are printed correctly.
Arnaud Spiwack
2014-09-04
*
Print [Variant] types with the keyword [Variant].
Arnaud Spiwack
2014-09-04
*
Add a [Variant] declaration which allows to write non-recursive variant types.
Arnaud Spiwack
2014-09-04
*
Fixing printing of unreachable local tactics.
Pierre-Marie Pédrot
2014-09-03
*
Cleaning code in Pptactic.
Pierre-Marie Pédrot
2014-09-02
*
Removing [revert] tactic from the AST.
Pierre-Marie Pédrot
2014-09-02
*
Moving the decompose tactic out of the AST.
Pierre-Marie Pédrot
2014-09-01
*
Coqide prints succesive hyps of the same type on 1 line
Pierre Boutillier
2014-09-01
*
Simplify even further the declaration of primitive projections,
Matthieu Sozeau
2014-08-30
[next]