aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-09-26Add a bunch of reproduction files for bugs.Xavier Clerc
2014-09-26Add missing "Fail" to bug cases.Xavier Clerc
2014-09-26Bug #3566 is fixed.Xavier Clerc
2014-09-26Adding a test for bug #3653.Pierre-Marie Pédrot
2014-09-26Test cases for closed bugs.Xavier Clerc
2014-09-25Fix incorrect assert false in detyping.Matthieu Sozeau
2014-09-25Revert changes of commit 4e1135fb315eab7 over file "plugins/micromega/sos.ml",Xavier Clerc
2014-09-25Add several reproduction files for bugs.Xavier Clerc
2014-09-25Improve consistency of whitespace (beautifier).Xavier Clerc
2014-09-25Remove some 'deprecated' warnings.Xavier Clerc
2014-09-25Hurkens.v: update comments.Arnaud Spiwack
2014-09-24Update test-suite files.Matthieu Sozeau
2014-09-24Rename eq_constr functions in Evd to not break backward compatibilityMatthieu Sozeau
2014-09-24Return a Prop not an arbitrary Type, and correct a typo.Matthieu Sozeau
2014-09-24Make eq_pattern_test/eq_test work up to the equivalence of primitiveMatthieu Sozeau
2014-09-24Using an or_var rather than the hack with loc for coding a pure identHugo Herbelin
2014-09-24Added support for interpreting hyp lists in tactic notations.Hugo Herbelin
2014-09-24Hurkens.v: show proofs in coqdoc.Arnaud Spiwack
2014-09-24Hurkens.v: a proof of [Type@{i}<>A] for any [A:Type@{i}].Arnaud Spiwack
2014-09-24Hurkens.v: coqdoc documentation.Arnaud Spiwack
2014-09-24A new version of Hurkens.v.Arnaud Spiwack
2014-09-24Make the retroknowledge marshalable.Arnaud Spiwack
2014-09-24Fix a message.Arnaud Spiwack
2014-09-24coqtop -emacs: do not declare "still unfocused goals" as an "infomsg".Arnaud Spiwack
2014-09-23Fix bug #3656.Matthieu Sozeau
2014-09-23ATBR can't compile without the fix, as it uses setoid_rewrite to rewriteMatthieu Sozeau
2014-09-23Fix bug in setoid_rewrite introduced by PMP's commits, which was creatingMatthieu Sozeau
2014-09-23adds general facts in the Reals library, whose need was detected inYves Bertot
2014-09-22Correction of error message (bug 3359)Julien Forest
2014-09-22Fixing bug 3951Julien Forest
2014-09-21Rewrite.apply_lemma is written in state passing style.Pierre-Marie Pédrot
2014-09-21More invariants in the code of Refine.Pierre-Marie Pédrot
2014-09-21Removing a nonsensical Errors.push.Pierre-Marie Pédrot
2014-09-19Move the specific map_constr_with_binders_left_to_rightMatthieu Sozeau
2014-09-19Fixes in Ltac pattern-matching on primitive projectionsMatthieu Sozeau
2014-09-19Use smart mapping in map_constr_with_binders_left_to_right.Matthieu Sozeau
2014-09-19Fixing bug #3646.Pierre-Marie Pédrot
2014-09-19win32: embed NSIS for plugin writersEnrico Tassi
2014-09-19Fixing #3641 (loop in e_contextually, introduced in r16525).Hugo Herbelin
2014-09-19Revert change of e_contextually as it needlessly expands all primitiveMatthieu Sozeau
2014-09-18Fix constrMatching as well as change/e_contextually to allowMatthieu Sozeau
2014-09-18Fix debug printing with primitive projections.Matthieu Sozeau
2014-09-18Do not try to match on a subterm that is not closed in find_subterm.Matthieu Sozeau
2014-09-18Clean a bit of univ.ml, add credits.Matthieu Sozeau
2014-09-18Fixing strange evarmap leak in goals.Pierre-Marie Pédrot
2014-09-18For type classes, tell that VarInstance's behave like GoalEvar (avoid a loop ...Hugo Herbelin
2014-09-18mltop: when a plugin is loaded store its full path in the summaryEnrico Tassi
2014-09-18Reductionops: (Co)Fixpoints are always refolded during iotaPierre Boutillier
2014-09-18fix coq_makefilePierre Boutillier
2014-09-18configure.ml: opam camlp5 + system ocaml worksPierre Boutillier
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-04 23:29:22 +0000