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
...
*
Fixing printing of induction/destruct as.
Hugo Herbelin
2016-04-27
*
Fixing printing of pat%constr.
Hugo Herbelin
2016-04-27
*
Honor parsing and printing levels for tactic entry in TACTIC EXTEND and
Hugo Herbelin
2016-04-27
*
Temporary deactivate re-interpretation of terms in beautify.
Hugo Herbelin
2016-04-27
*
In the short term, stronger invariant on the syntax of TacAssert, what
Hugo Herbelin
2016-04-27
*
So as to beautify to work, do not use notations in Inductive types
Hugo Herbelin
2016-04-27
*
A heuristic to add parentheses in the presence of rules such as
Hugo Herbelin
2016-04-27
*
Attempt to slightly improve abusive "Collision between bound
Hugo Herbelin
2016-04-27
*
Removing dead code related to printing of ML tactics in Pptactic.
Pierre-Marie Pédrot
2016-04-25
*
Moving and enhancing the grammar_tactic_prod_item_expr type.
Pierre-Marie Pédrot
2016-04-14
*
Fixing printing of "destruct in" after ce71ac17268f.
Hugo Herbelin
2016-04-12
*
Removing the ad-hoc tactic_expr type.
Pierre-Marie Pédrot
2016-04-11
*
Extruding the print_atom primitive.
Pierre-Marie Pédrot
2016-04-10
*
Removing extra spaces in printing arguments of VERNAC EXTEND.
Hugo Herbelin
2016-04-09
*
Removing automatic printing of leading space in auto_using and
Hugo Herbelin
2016-04-09
*
Simplifying code for printing VERNAC EXTEND.
Hugo Herbelin
2016-04-09
*
Fixing extra space in printing inductive types with no explicit type given.
Hugo Herbelin
2016-04-09
*
In pr_clauses, do not print a leading space by default so that it can
Hugo Herbelin
2016-04-09
*
Fixing printing of toplevel values.
Pierre-Marie Pédrot
2016-04-08
*
Fixing printing of Tactic Notations with tactic arguments.
Pierre-Marie Pédrot
2016-04-08
*
Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...
Matthieu Sozeau
2016-04-04
|
\
*
\
Merge branch 'linear-comparison' of https://github.com/aspiwack/coq into aspi...
Matthieu Sozeau
2016-04-04
|
\
\
*
\
\
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-30
|
\
\
\
|
*
|
|
Univs: fix get_current_context (bug #4603, part I)
Matthieu Sozeau
2016-03-25
*
|
|
|
Adding a new Ltac generic argument for forced tactics returing unit.
Pierre-Marie Pédrot
2016-03-20
*
|
|
|
Moving Refine to its proper module.
Pierre-Marie Pédrot
2016-03-20
*
|
|
|
Moving the Ltac definition command to an EXTEND based command.
Pierre-Marie Pédrot
2016-03-20
*
|
|
|
Moving Print Ltac to an EXTEND based command.
Pierre-Marie Pédrot
2016-03-20
*
|
|
|
Moving Tactic Notation to an EXTEND based command.
Pierre-Marie Pédrot
2016-03-20
*
|
|
|
Removing the untyped representation of genargs.
Pierre-Marie Pédrot
2016-03-19
*
|
|
|
Moving VernacSolve to an EXTEND-based definition.
Pierre-Marie Pédrot
2016-03-19
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-18
|
\
|
|
|
*
|
|
|
Supporting "(@foo) args" in patterns, where "@foo" has no arguments.
Hugo Herbelin
2016-03-13
|
*
|
|
Primitive projections: protect kernel from erroneous definitions.
Matthieu Sozeau
2016-03-10
*
|
|
|
Moving Autorewrite to Hightatctic.
Pierre-Marie Pédrot
2016-03-06
*
|
|
|
Moving Tactic_debug to tactics/ folder.
Pierre-Marie Pédrot
2016-03-06
*
|
|
|
Removing the UConstr entry of the tactic_arg AST.
Pierre-Marie Pédrot
2016-03-04
*
|
|
|
Moving the "move" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
|
|
Moving the "exists" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
|
|
Moving the "symmetry" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
|
|
Moving the "generalize dependent" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
|
|
Moving the "clearbody" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
|
|
Moving the "clear" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
|
|
Moving the "cofix" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
|
|
Moving the "fix" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
|
|
Removing the MetaIdArg entry of tactic expressions.
Pierre-Marie Pédrot
2016-02-24
*
|
|
|
The tactic generic argument now returns a value rather than a glob_expr.
Pierre-Marie Pédrot
2016-02-22
*
|
|
|
merging conflicts with the original "trunk__CLEANUP__Context__2" branch
Matej Kosik
2016-02-15
|
\
\
\
\
*
\
\
\
\
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-02-13
|
\
\
\
\
\
|
|
|
/
/
/
|
|
/
|
|
|
|
*
|
|
|
Do not give a name to anonymous evars anymore. See bug #4547.
Pierre-Marie Pédrot
2016-02-13
[prev]
[next]
Hugo Herbelin
Pierre-Marie Pédrot
Matthieu Sozeau
Matthieu Sozeau
Matej Kosik