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
*
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
*
Fix bug #3593, making constr_eq and progress work up to
Matthieu Sozeau
2014-09-17
*
Fix bug #3633 properly, by delaying the interpetation of constrs in
Matthieu Sozeau
2014-09-17
*
Change some Defined into Qed.
Guillaume Melquiond
2014-09-17
*
Add some missing Proof statements.
Guillaume Melquiond
2014-09-17
*
Remove pointless regex for '""' as the empty string already matches it.
Guillaume Melquiond
2014-09-17
*
Revert "coqc: execvp is now available even on win32"
Enrico Tassi
2014-09-17
*
win32: remove outdated splash screen
Enrico Tassi
2014-09-17
*
Fix highlighting of "Hint Unfold" and "Hint Rewrite".
Guillaume Melquiond
2014-09-17
*
Properly highlight the Export keyword.
Guillaume Melquiond
2014-09-17
*
Fix ambiguous regex in syntax highlighting.
Guillaume Melquiond
2014-09-17
*
Change an axiom into a definition.
Guillaume Melquiond
2014-09-17
*
Fix broken syntax highlighting for Coq files using "Proof constr".
Guillaume Melquiond
2014-09-17
[next]