| Age | Commit message (Expand) | Author |
|---|
| 2014-09-25 | 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-24 | 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-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 |
