index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
...
*
So as to beautify to work, do not use notations in Inductive types
Hugo Herbelin
2016-06-16
*
Fixing missing substitution / printing cases of TacSelect.
Pierre-Marie Pédrot
2016-06-16
*
Fixing parsing of constr argument of ltac functions at level 8 in the
Hugo Herbelin
2016-06-16
*
Fixing printing of keeping hyp on the fly.
Hugo Herbelin
2016-06-16
*
Fixing printing of inversion as.
Hugo Herbelin
2016-06-16
*
Fixing extra space in printing destruct/induction as.
Hugo Herbelin
2016-06-16
*
Fixing printing of induction/destruct as.
Hugo Herbelin
2016-06-16
*
Fixing printing of pat%constr.
Hugo Herbelin
2016-06-16
*
In NMake_gen, giving to tactic do_size a grammar rule which respects the levels.
Hugo Herbelin
2016-06-16
*
Adding option "Set Reversible Pattern Implicit" to Specif.v so that an
Hugo Herbelin
2016-06-16
*
Being defensive in printing implicit arguments also with manual
Hugo Herbelin
2016-06-16
*
A stronger invariant on the syntax of TacAssert, what allows for a
Hugo Herbelin
2016-06-16
*
Changing rule for "*" in Operator_Properties so that, iterated, it
Hugo Herbelin
2016-06-16
*
Protect the beautifier from change in the lexer state (typically by
Hugo Herbelin
2016-06-16
*
Not taking arguments given by name or position into account when
Hugo Herbelin
2016-06-16
*
Merge '/pr/206' into trunk
Enrico Tassi
2016-06-16
|
\
*
\
Merge PR #195: Complete is_* family of term-examining tactics.
Pierre-Marie Pédrot
2016-06-16
|
\
\
*
\
\
Merge 'pr/191' into trunk
Enrico Tassi
2016-06-16
|
\
\
\
*
\
\
\
Merge PR #211: Fix a printing typo in LtacProf.
Pierre-Marie Pédrot
2016-06-16
|
\
\
\
\
*
\
\
\
\
Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.
Pierre-Marie Pédrot
2016-06-16
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #100: fresh now accepts more things than just identifiers.
Pierre-Marie Pédrot
2016-06-16
|
\
\
\
\
\
\
*
|
|
|
|
|
|
Fix Makefile after ssrmatching merge
Enrico Tassi
2016-06-16
*
|
|
|
|
|
|
--print-version produces machine readable version info
Enrico Tassi
2016-06-16
*
|
|
|
|
|
|
ideslave: do not bail out in case of XML error
Enrico Tassi
2016-06-16
*
|
|
|
|
|
|
Remove inappropriate comment.
Maxime Dénès
2016-06-16
|
|
|
|
|
*
|
Update CHANGES
Jason Gross
2016-06-16
|
|
|
|
|
*
|
Add is_const
Jason Gross
2016-06-16
*
|
|
|
|
|
|
Merge branch 'pr/146' into trunk
Enrico Tassi
2016-06-16
|
\
\
\
\
\
\
\
|
*
|
|
|
|
|
|
Ignore generated .ml file for ssrmatching
Enrico Tassi
2016-06-16
*
|
|
|
|
|
|
|
Merge remote-tracking branch 'github/pr/194' into trunk
Maxime Dénès
2016-06-16
|
\
\
\
\
\
\
\
\
|
|
|
|
|
*
|
|
|
Fix another missing newline
Jason Gross
2016-06-16
|
|
|
|
|
*
|
|
|
Fix a printing typo
Jason Gross
2016-06-16
|
|
_
|
_
|
_
|
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
Fixing the checker.
Pierre-Marie Pédrot
2016-06-16
|
|
|
|
*
|
|
|
Remove the syntax changes introduced by this branch.
Pierre-Marie Pédrot
2016-06-15
*
|
|
|
|
|
|
|
Fix test-suite for opened bug #4813.
Pierre-Marie Pédrot
2016-06-15
|
|
|
|
*
|
|
|
Allow `Pretyping.search_guard` to not check guard
Arnaud Spiwack
2016-06-15
|
|
*
|
|
|
|
|
ssrmatching: giving proper credits to the original author(s)
Enrico Tassi
2016-06-15
|
|
*
|
|
|
|
|
Merge branch 'pr/146' into trunk
Enrico Tassi
2016-06-15
|
|
/
|
|
|
|
|
|
|
/
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
ssrmatching: simple test for Ltac API
Enrico Tassi
2016-06-15
|
|
*
|
|
|
|
|
ssrmatching: ltac argument parsing made more robust
Enrico Tassi
2016-06-15
|
|
*
|
|
|
|
|
ssrmatching: debug prints sent via msg_debug
Enrico Tassi
2016-06-15
|
|
*
|
|
|
|
|
Rename "Set SsrMatchingDebug" into "Set Debug SsrMatching"
Enrico Tassi
2016-06-15
*
|
|
|
|
|
|
|
typography
Matej Kosik
2016-06-15
*
|
|
|
|
|
|
|
ocamllibdep + coqdep : simpler deps concerning .mllib and .mlpack
Pierre Letouzey
2016-06-15
*
|
|
|
|
|
|
|
Makefile.build: ensure a build failure in case of a missing rule
Pierre Letouzey
2016-06-15
*
|
|
|
|
|
|
|
fix test-suite/ide Makefile (stupid typo)
Enrico Tassi
2016-06-15
|
|
|
|
*
|
|
|
Assume totality: dedicated type rather than bool
Arnaud Spiwack
2016-06-14
*
|
|
|
|
|
|
|
Preventive compatibility fixes for flushing.
Emilio Jesus Gallego Arias
2016-06-14
*
|
|
|
|
|
|
|
Fix for bug #4784
Emilio Jesus Gallego Arias
2016-06-14
*
|
|
|
|
|
|
|
Repair the build of ide/coqidetop.cmxs (fix #4812)
Pierre Letouzey
2016-06-14
[prev]
[next]