| Commit message (Expand) | Author | Age |
... | |
* | 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 |
* | 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 |