aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2014-09-27Bug fixed.Matthieu Sozeau
2014-09-27Make pattern_of_constr typed so that we can infer the proper patternsMatthieu Sozeau
for primitive projections, fixing bug #3661. Also fix expand_projection so that it does enough reduction to find the inductive type of its argument.
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
so as to reproduce correctly the reduction behavior of existing projections, i.e. delta + iota. Make [projection] an abstract datatype in Names.ml, most of the patch is about using that abstraction. Fix unification.ml which tried canonical projections too early in presence of primitive projections.
2014-09-27Adapting to naming of evars.Hugo Herbelin
2014-09-27Changed semantics of induction !id when a clause is given: don'tHugo Herbelin
authoritatively erase non-generalized hypotheses dependent on id.
2014-09-27Removing the last use of tclSENSITIVE in favour of tclNEWGOALS.Pierre-Marie Pédrot
Most of the code from Goal.Refine and related was moved to the one file that was using it, wiz. tactics.ml. Some additional care should be taken to clean up even more the remaining code.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 08:00:30 +0000