aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2014-09-26Adding a tclNEWGOALS primitive.Pierre-Marie Pédrot
2014-09-26Hurkens.v: Fix a syntax error.Arnaud Spiwack
Introduced in c74a70a73b3bf39394c551f1cdb224450bf77176.
2014-09-26Fix canonical structure resolution which was launched on the results ofMatthieu Sozeau
eta-expansion, creating a loop. This is now deactivated. Fixes bugs #3665 and #3667.
2014-09-26ClassicalFacts: adds a proof that weak excluded middle implies weak proof ↵Arnaud Spiwack
irrelevance. Application of previous commit in Hurkens.v.
2014-09-26Hurkens.v: new paradox: type of modal propositions is not a retract.Arnaud Spiwack
In particular there is no retract of the type of negative propositions in a negative proposition.
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
as "||" is actually redefined in "plugins/micromega/sos_lib.ml".
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
with existing ML code.
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
projections with their eta-expanded constant form.
2014-09-24Using an or_var rather than the hack with loc for coding a pure identHugo Herbelin
as a disjunctive intropattern.
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
Adds a more generic and modular proof of Hurkens, where a shallow embedding of U- is given in the most general way. Subsumes all the previous proofs, opens the way to new proofs.
2014-09-24Make the retroknowledge marshalable.Arnaud Spiwack
Essential for parallel processing of Coq documents. It is a fairly straightforward change but a tad tedious, I may have introduced some bugs in the process.
2014-09-24Fix a message.Arnaud Spiwack
2014-09-24coqtop -emacs: do not declare "still unfocused goals" as an "infomsg".Arnaud Spiwack
This prevented the message from being silent when jumping ahead in a file. Fixes #3636.
2014-09-23Fix bug #3656.Matthieu Sozeau
Maintain the user-level view of primitive projections, disallow manual unfolding and do not let hnf give the eta-expanded form.
2014-09-23ATBR can't compile without the fix, as it uses setoid_rewrite to rewriteMatthieu Sozeau
under binders. This might incur a significant time penalty.
2014-09-23Fix bug in setoid_rewrite introduced by PMP's commits, which was creatingMatthieu Sozeau
two versions of the rewriting lemma, keeping useless evars around. This can now happen only when the rewrite lemma is used under binders... Fix to do next.
2014-09-23adds general facts in the Reals library, whose need was detected inYves Bertot
experiments about computing PI
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
This removes a use of Evd.merge.
2014-09-21More invariants in the code of Refine.Pierre-Marie Pédrot
The hypinfo state is now refreshed at a proper time, which should reduce the overall number of calls to [decompose_applied_relation]. The state passing nature of the program is also more explicit, removing a use of Evd.merge. This patch should preserve semantics and efficiency.
2014-09-21Removing a nonsensical Errors.push.Pierre-Marie Pédrot
2014-09-19Move the specific map_constr_with_binders_left_to_rightMatthieu Sozeau
for e_contextually where it is used. Bug #3648 is fixed.
2014-09-19Fixes in Ltac pattern-matching on primitive projectionsMatthieu Sozeau
and pretyping which was not contracting the eta-expanded forms in presence of coercions.
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
projections in the term.
2014-09-18Fix constrMatching as well as change/e_contextually to allowMatthieu Sozeau
matching partial applications of primitive projections. Fixes bug #3637.
2014-09-18Fix debug printing with primitive projections.Matthieu Sozeau
Add a flag to indicate if we're in the toplevel or debuggger to not try to retype terms in the wrong environment (and making find_rectype, get_type_of untraceable). This fixes bug #3638 along with the previous commit.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 22:29:05 +0000