aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-09-29In evarconv and unification, expand folded primitive projections toMatthieu Sozeau
2014-09-28Print information about primitive records (Print and About).Matthieu Sozeau
2014-09-27Keyed unification option, compiling the whole standard libraryMatthieu Sozeau
2014-09-27Index keys instead of simply global references.Matthieu Sozeau
2014-09-27First version of keyed subterm selection in unification.Matthieu Sozeau
2014-09-27Fix test-suite file.Matthieu Sozeau
2014-09-27Fix bug #3664 by refolding projections that don't reduce in cbn.Matthieu Sozeau
2014-09-27Remove auto's use of dummy goal, use the proper sigma for pattern_of_constr.Matthieu Sozeau
2014-09-27Fix semantics of matching with folded/unfolded projections to definitelyMatthieu Sozeau
2014-09-27Fix bug #3672, application of primitive projections as coercions.Matthieu Sozeau
2014-09-27Fix bug 3662 by actually reducing primitive projections in cbv/compute.Matthieu Sozeau
2014-09-27Bug fixed.Matthieu Sozeau
2014-09-27Make pattern_of_constr typed so that we can infer the proper patternsMatthieu Sozeau
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-09-27Adapting to naming of evars.Hugo Herbelin
2014-09-27Changed semantics of induction !id when a clause is given: don'tHugo Herbelin
2014-09-27Removing the last use of tclSENSITIVE in favour of tclNEWGOALS.Pierre-Marie Pédrot
2014-09-26Adding a tclNEWGOALS primitive.Pierre-Marie Pédrot
2014-09-26Hurkens.v: Fix a syntax error.Arnaud Spiwack
2014-09-26Fix canonical structure resolution which was launched on the results ofMatthieu Sozeau
2014-09-26ClassicalFacts: adds a proof that weak excluded middle implies weak proof irr...Arnaud Spiwack
2014-09-26Hurkens.v: new paradox: type of modal propositions is not a retract.Arnaud Spiwack
2014-09-26Hurkens.v: fix coqdoc formatting in a comment.Arnaud Spiwack
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 20:44:33 +0000