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
...
*
|
Removing constr generic argument.
Pierre-Marie Pédrot
2016-01-14
*
|
Removing ident and var generic arguments.
Pierre-Marie Pédrot
2016-01-14
*
|
Moving is_quantified_hypothesis to new proof engine.
Hugo Herbelin
2016-01-14
*
|
Updating and improving the documentation of intros patterns.
Hugo Herbelin
2016-01-14
*
|
Continuing 003fe3d5e on parsing positions.
Hugo Herbelin
2016-01-14
*
|
Changing "P is assumed" to "P is declared".
Hugo Herbelin
2016-01-14
*
|
Update in the documentation of parts of the code of destruct/induction.
Hugo Herbelin
2016-01-14
|
*
MMaps: remove it from final 8.5 release, since this new library isn't mature ...
Pierre Letouzey
2016-01-13
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-13
|
\
|
|
*
Fixing success of test for #3848 after move to directory "closed".
Hugo Herbelin
2016-01-13
|
*
Fixing #4467 (continued).
Hugo Herbelin
2016-01-13
|
*
Fixing #4467 (missing shadowing of variables in cases pattern).
Hugo Herbelin
2016-01-12
|
*
Fixing #4256 and #4484 (changes in evar-evar resolution made that new
Hugo Herbelin
2016-01-12
|
*
Reporting about the new tactical unshelve.
Hugo Herbelin
2016-01-12
|
*
Extend last commit: keyed unification uses full conversions on the applied co...
Matthieu Sozeau
2016-01-12
|
*
Extend Keyed Unification tests with the one from R. Krebbers.
Matthieu Sozeau
2016-01-12
|
*
Fix essential bug in new Keyed Unification mode reported by R. Krebbers.
Matthieu Sozeau
2016-01-12
|
*
Referring to coq.inria.fr/stdlib for more on libraries and ltac-level tactics.
Hugo Herbelin
2016-01-12
|
*
Documenting dtauto and dintuition.
Hugo Herbelin
2016-01-12
|
*
Documenting options "Intuition Negation Unfolding", "Intuition Iff Unfolding".
Hugo Herbelin
2016-01-12
|
*
Documenting option 'Set Bracketing Last Introduction Pattern'.
Hugo Herbelin
2016-01-12
|
*
restore documentation of admit
Enrico Tassi
2016-01-12
*
|
CLEANUP: removing unnecessary wrapper
Matej Kosik
2016-01-11
*
|
COMMENTS: added to the "Constrexpr.CCases" variant.
Matej Kosik
2016-01-11
*
|
CLEANUP: removing unused field
Matej Kosik
2016-01-11
*
|
merge
Matej Kosik
2016-01-11
|
\
\
|
*
|
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
|
|
*
Fix bug #3338 again, no progress is necessary for the success of rewrite_strat.
Matthieu Sozeau
2016-01-11
*
|
|
COMMENTS: of "Constr.case_info" type were updated.
Matej Kosik
2016-01-11
*
|
|
COMMENTS: added to the "Names.inductive" and "Names.constructor" types.
Matej Kosik
2016-01-11
*
|
|
Fix bug 4479: "Error: Rewriting base foo does not exist." should be catchable.
Pierre-Marie Pédrot
2016-01-09
*
|
|
Monotonizing Ftactic.
Pierre-Marie Pédrot
2016-01-08
|
|
*
Be more verbose about failure to compile libraries to native code.
Guillaume Melquiond
2016-01-08
|
|
*
Fix a misleading comment for substn_vars
Matthieu Sozeau
2016-01-07
|
|
*
Fix bug #4480: progress was not checked for setoid_rewrite.
Matthieu Sozeau
2016-01-07
|
|
*
Fix description of command-line options in the manual.
Guillaume Melquiond
2016-01-06
*
|
|
Remove deprecated command-line options such as "-as".
Guillaume Melquiond
2016-01-06
*
|
|
Make code more readable by not mixing list traversal and option processing.
Guillaume Melquiond
2016-01-06
*
|
|
Merge remote-tracking branch 'origin/v8.5' into trunk
Guillaume Melquiond
2016-01-06
|
\
\
\
|
|
|
/
|
|
/
|
|
*
|
Prevent coq_makefile from parsing project files in the reverse order. (Fix bu...
Guillaume Melquiond
2016-01-06
|
*
|
Protect code against changes in Map interface.
Maxime Dénès
2016-01-06
|
*
|
Disable warning 31 when generating coqtop from coqmktop.
Maxime Dénès
2016-01-05
*
|
|
Merge remote-tracking branch 'origin/v8.5' into trunk
Guillaume Melquiond
2016-01-05
|
\
\
\
|
|
*
|
Avoid warning 31: test printer was linked twice with Dynlink and Str.
Maxime Dénès
2016-01-05
|
|
*
|
Fix order of files in mllib.
Maxime Dénès
2016-01-05
|
|
/
/
|
*
|
COMMENTS: Predicate
Matej Kosik
2016-01-05
|
*
|
fixup d2b468a, evar normalization is needed
Enrico Tassi
2016-01-04
|
*
|
Extraction: msg_notice instead of msg_info.
Pierre Courtieu
2016-01-04
|
*
|
Fix handling of side-effects in case of `Opaque side-effects as well.
Matthieu Sozeau
2016-01-04
|
*
|
par: check if the goal is not ground and fail (fix #4465)
Enrico Tassi
2016-01-04
[prev]
[next]