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
*
Bug #3566 is fixed.
Xavier Clerc
2014-09-26
*
Adding a test for bug #3653.
Pierre-Marie Pédrot
2014-09-26
*
Test cases for closed bugs.
Xavier Clerc
2014-09-26
*
Fix incorrect assert false in detyping.
Matthieu Sozeau
2014-09-25
*
Revert changes of commit 4e1135fb315eab7 over file "plugins/micromega/sos.ml",
Xavier Clerc
2014-09-25
*
Add several reproduction files for bugs.
Xavier Clerc
2014-09-25
*
Improve consistency of whitespace (beautifier).
Xavier Clerc
2014-09-25
*
Remove some 'deprecated' warnings.
Xavier Clerc
2014-09-25
*
Hurkens.v: update comments.
Arnaud Spiwack
2014-09-25
*
Update test-suite files.
Matthieu Sozeau
2014-09-24
*
Rename eq_constr functions in Evd to not break backward compatibility
Matthieu Sozeau
2014-09-24
*
Return a Prop not an arbitrary Type, and correct a typo.
Matthieu Sozeau
2014-09-24
*
Make eq_pattern_test/eq_test work up to the equivalence of primitive
Matthieu Sozeau
2014-09-24
*
Using an or_var rather than the hack with loc for coding a pure ident
Hugo Herbelin
2014-09-24
*
Added support for interpreting hyp lists in tactic notations.
Hugo Herbelin
2014-09-24
*
Hurkens.v: show proofs in coqdoc.
Arnaud Spiwack
2014-09-24
*
Hurkens.v: a proof of [Type@{i}<>A] for any [A:Type@{i}].
Arnaud Spiwack
2014-09-24
*
Hurkens.v: coqdoc documentation.
Arnaud Spiwack
2014-09-24
*
A new version of Hurkens.v.
Arnaud Spiwack
2014-09-24
*
Make the retroknowledge marshalable.
Arnaud Spiwack
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 bug #3656.
Matthieu Sozeau
2014-09-23
*
ATBR can't compile without the fix, as it uses setoid_rewrite to rewrite
Matthieu Sozeau
2014-09-23
*
Fix bug in setoid_rewrite introduced by PMP's commits, which was creating
Matthieu Sozeau
2014-09-23
*
adds general facts in the Reals library, whose need was detected in
Yves Bertot
2014-09-23
*
Correction of error message (bug 3359)
Julien Forest
2014-09-22
*
Fixing bug 3951
Julien Forest
2014-09-22
*
Rewrite.apply_lemma is written in state passing style.
Pierre-Marie Pédrot
2014-09-21
*
More invariants in the code of Refine.
Pierre-Marie Pédrot
2014-09-21
*
Removing a nonsensical Errors.push.
Pierre-Marie Pédrot
2014-09-21
*
Move the specific map_constr_with_binders_left_to_right
Matthieu Sozeau
2014-09-19
*
Fixes in Ltac pattern-matching on primitive projections
Matthieu Sozeau
2014-09-19
*
Use smart mapping in map_constr_with_binders_left_to_right.
Matthieu Sozeau
2014-09-19
*
Fixing bug #3646.
Pierre-Marie Pédrot
2014-09-19
*
win32: embed NSIS for plugin writers
Enrico Tassi
2014-09-19
*
Fixing #3641 (loop in e_contextually, introduced in r16525).
Hugo Herbelin
2014-09-19
*
Revert change of e_contextually as it needlessly expands all primitive
Matthieu Sozeau
2014-09-19
*
Fix constrMatching as well as change/e_contextually to allow
Matthieu Sozeau
2014-09-18
*
Fix debug printing with primitive projections.
Matthieu Sozeau
2014-09-18
*
Do not try to match on a subterm that is not closed in find_subterm.
Matthieu Sozeau
2014-09-18
*
Clean a bit of univ.ml, add credits.
Matthieu Sozeau
2014-09-18
*
Fixing strange evarmap leak in goals.
Pierre-Marie Pédrot
2014-09-18
*
For type classes, tell that VarInstance's behave like GoalEvar (avoid a loop ...
Hugo Herbelin
2014-09-18
*
mltop: when a plugin is loaded store its full path in the summary
Enrico Tassi
2014-09-18
*
Reductionops: (Co)Fixpoints are always refolded during iota
Pierre Boutillier
2014-09-18
*
fix coq_makefile
Pierre Boutillier
2014-09-18
*
configure.ml: opam camlp5 + system ocaml works
Pierre Boutillier
2014-09-18
*
seems to fix a looping coq-tex (when compiled with camlp4)
Pierre Boutillier
2014-09-18
*
Be more conservative and keep the use of eq_constr in pretyping/ functions.
Matthieu Sozeau
2014-09-17
[next]