| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-09-26 | Test cases for closed bugs. | Xavier Clerc | |
| 2014-09-25 | Fix incorrect assert false in detyping. | Matthieu Sozeau | |
| 2014-09-25 | Revert changes of commit 4e1135fb315eab7 over file "plugins/micromega/sos.ml", | Xavier Clerc | |
| as "||" is actually redefined in "plugins/micromega/sos_lib.ml". | |||
| 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-24 | Update test-suite files. | Matthieu Sozeau | |
| 2014-09-24 | Rename eq_constr functions in Evd to not break backward compatibility | Matthieu Sozeau | |
| with existing ML code. | |||
| 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 | |
| projections with their eta-expanded constant form. | |||
| 2014-09-24 | Using an or_var rather than the hack with loc for coding a pure ident | Hugo Herbelin | |
| as a disjunctive intropattern. | |||
| 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 | |
| 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-24 | Make 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-24 | Fix a message. | Arnaud Spiwack | |
| 2014-09-24 | coqtop -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-23 | Fix 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-23 | ATBR can't compile without the fix, as it uses setoid_rewrite to rewrite | Matthieu Sozeau | |
| under binders. This might incur a significant time penalty. | |||
| 2014-09-23 | Fix bug in setoid_rewrite introduced by PMP's commits, which was creating | Matthieu 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-23 | adds general facts in the Reals library, whose need was detected in | Yves Bertot | |
| experiments about computing PI | |||
| 2014-09-22 | Correction of error message (bug 3359) | Julien Forest | |
| 2014-09-22 | Fixing bug 3951 | Julien Forest | |
| 2014-09-21 | Rewrite.apply_lemma is written in state passing style. | Pierre-Marie Pédrot | |
| This removes a use of Evd.merge. | |||
| 2014-09-21 | More 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-21 | Removing a nonsensical Errors.push. | Pierre-Marie Pédrot | |
| 2014-09-19 | Move the specific map_constr_with_binders_left_to_right | Matthieu Sozeau | |
| for e_contextually where it is used. Bug #3648 is fixed. | |||
| 2014-09-19 | Fixes in Ltac pattern-matching on primitive projections | Matthieu Sozeau | |
| and pretyping which was not contracting the eta-expanded forms in presence of coercions. | |||
| 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 | |
| projections in the term. | |||
| 2014-09-18 | Fix constrMatching as well as change/e_contextually to allow | Matthieu Sozeau | |
| matching partial applications of primitive projections. Fixes bug #3637. | |||
| 2014-09-18 | Fix 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-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 | |
| Goals have to be refreshed when observed, because the evarmap may have changed between the moment where the goal was generated and the moment the goal is used. | |||
| 2014-09-18 | For type classes, tell that VarInstance's behave like GoalEvar (avoid a loop ↵ | Hugo Herbelin | |
| in Class_tactics). | |||
| 2014-09-18 | mltop: when a plugin is loaded store its full path in the summary | Enrico Tassi | |
| This fixes the following bug related to stm: if one passes -I to coqide, then such flag is passes to the workers; but if one uses "Add ML LoadPath" to extend the paths in which coq looks for plugins, this extra path was no passed to the slaves (via the command line) nor store in the system state and hence sent to the slaves. With this patch, when a cmxs is loaded, its full path is stored in the summary and hence sent to the workers as one may expect. | |||
| 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 | |
| I didn't understand the purpose of the previous behavior so please check this commit | |||
| 2014-09-18 | seems to fix a looping coq-tex (when compiled with camlp4) | Pierre Boutillier | |
| 2014-09-17 | 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 | |
| equality of universes, along with a few other functions in evd. | |||
| 2014-09-17 | Fix bug #3633 properly, by delaying the interpetation of constrs in | Matthieu Sozeau | |
| apply f, g,... so that apply f, g. succeeds when apply f; apply g does. It just mimicks the behavior of rewrite foo bar. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |