| Age | Commit message (Expand) | Author |
|---|
| 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-23 | 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-22 | Correction of error message (bug 3359) | Julien Forest |
| 2014-09-22 | Fixing bug 3951 | Julien Forest |
| 2014-09-21 | 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-19 | 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-18 | 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-17 | 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 | win32: bring back the coq icon in the coqide binary | Enrico Tassi |
| 2014-09-17 | win32: use subsystem windows on windows (and not console) | Enrico Tassi |
| 2014-09-17 | Revert "While resolving typeclass evars in clenv, touch only the ones that ap... | Matthieu Sozeau |
| 2014-09-17 | While resolving typeclass evars in clenv, touch only the ones that appear in the | Matthieu Sozeau |
| 2014-09-17 | Update test-suite files after last commit. Add a file for rewrite_strat | Matthieu Sozeau |
