aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Using an or_var rather than the hack with loc for coding a pure identGravatar Hugo Herbelin2014-09-24
| | | | as a disjunctive intropattern.
* Added support for interpreting hyp lists in tactic notations.Gravatar Hugo Herbelin2014-09-24
|
* Hurkens.v: show proofs in coqdoc.Gravatar Arnaud Spiwack2014-09-24
|
* Hurkens.v: a proof of [Type@{i}<>A] for any [A:Type@{i}].Gravatar Arnaud Spiwack2014-09-24
|
* Hurkens.v: coqdoc documentation.Gravatar Arnaud Spiwack2014-09-24
|
* A new version of Hurkens.v.Gravatar Arnaud Spiwack2014-09-24
| | | | 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.
* Make the retroknowledge marshalable.Gravatar Arnaud Spiwack2014-09-24
| | | | | | 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.
* Fix a message.Gravatar Arnaud Spiwack2014-09-24
|
* coqtop -emacs: do not declare "still unfocused goals" as an "infomsg".Gravatar Arnaud Spiwack2014-09-24
| | | This prevented the message from being silent when jumping ahead in a file. Fixes #3636.
* Fix bug #3656.Gravatar Matthieu Sozeau2014-09-23
| | | | | | Maintain the user-level view of primitive projections, disallow manual unfolding and do not let hnf give the eta-expanded form.
* ATBR can't compile without the fix, as it uses setoid_rewrite to rewriteGravatar Matthieu Sozeau2014-09-23
| | | | under binders. This might incur a significant time penalty.
* Fix bug in setoid_rewrite introduced by PMP's commits, which was creatingGravatar Matthieu Sozeau2014-09-23
| | | | | | 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.
* adds general facts in the Reals library, whose need was detected inGravatar Yves Bertot2014-09-23
| | | | experiments about computing PI
* Correction of error message (bug 3359)Gravatar Julien Forest2014-09-22
|
* Fixing bug 3951Gravatar Julien Forest2014-09-22
|
* Rewrite.apply_lemma is written in state passing style.Gravatar Pierre-Marie Pédrot2014-09-21
| | | | This removes a use of Evd.merge.
* More invariants in the code of Refine.Gravatar Pierre-Marie Pédrot2014-09-21
| | | | | | | 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.
* Removing a nonsensical Errors.push.Gravatar Pierre-Marie Pédrot2014-09-21
|
* Move the specific map_constr_with_binders_left_to_rightGravatar Matthieu Sozeau2014-09-19
| | | | for e_contextually where it is used. Bug #3648 is fixed.
* Fixes in Ltac pattern-matching on primitive projectionsGravatar Matthieu Sozeau2014-09-19
| | | | | and pretyping which was not contracting the eta-expanded forms in presence of coercions.
* Use smart mapping in map_constr_with_binders_left_to_right.Gravatar Matthieu Sozeau2014-09-19
|
* Fixing bug #3646.Gravatar Pierre-Marie Pédrot2014-09-19
|
* win32: embed NSIS for plugin writersGravatar Enrico Tassi2014-09-19
|
* Fixing #3641 (loop in e_contextually, introduced in r16525).Gravatar Hugo Herbelin2014-09-19
|
* Revert change of e_contextually as it needlessly expands all primitiveGravatar Matthieu Sozeau2014-09-19
| | | | projections in the term.
* Fix constrMatching as well as change/e_contextually to allowGravatar Matthieu Sozeau2014-09-18
| | | | matching partial applications of primitive projections. Fixes bug #3637.
* Fix debug printing with primitive projections.Gravatar Matthieu Sozeau2014-09-18
| | | | | | | 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.
* Do not try to match on a subterm that is not closed in find_subterm.Gravatar Matthieu Sozeau2014-09-18
|
* Clean a bit of univ.ml, add credits.Gravatar Matthieu Sozeau2014-09-18
|
* Fixing strange evarmap leak in goals.Gravatar Pierre-Marie Pédrot2014-09-18
| | | | | | 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.
* For type classes, tell that VarInstance's behave like GoalEvar (avoid a loop ↵Gravatar Hugo Herbelin2014-09-18
| | | | in Class_tactics).
* mltop: when a plugin is loaded store its full path in the summaryGravatar Enrico Tassi2014-09-18
| | | | | | | | | | | 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.
* Reductionops: (Co)Fixpoints are always refolded during iotaGravatar Pierre Boutillier2014-09-18
|
* fix coq_makefileGravatar Pierre Boutillier2014-09-18
|
* configure.ml: opam camlp5 + system ocaml worksGravatar Pierre Boutillier2014-09-18
| | | | I didn't understand the purpose of the previous behavior so please check this commit
* seems to fix a looping coq-tex (when compiled with camlp4)Gravatar Pierre Boutillier2014-09-18
|
* Be more conservative and keep the use of eq_constr in pretyping/ functions.Gravatar Matthieu Sozeau2014-09-17
|
* Fix bug #3593, making constr_eq and progress work up toGravatar Matthieu Sozeau2014-09-17
| | | | equality of universes, along with a few other functions in evd.
* Fix bug #3633 properly, by delaying the interpetation of constrs inGravatar Matthieu Sozeau2014-09-17
| | | | | apply f, g,... so that apply f, g. succeeds when apply f; apply g does. It just mimicks the behavior of rewrite foo bar.
* Change some Defined into Qed.Gravatar Guillaume Melquiond2014-09-17
|
* Add some missing Proof statements.Gravatar Guillaume Melquiond2014-09-17
|
* Remove pointless regex for '""' as the empty string already matches it.Gravatar Guillaume Melquiond2014-09-17
|
* Revert "coqc: execvp is now available even on win32"Gravatar Enrico Tassi2014-09-17
| | | | | | | | | This reverts commit 60c390951cb2d771c16758a84bf592d06769da14. The reason is that execvp exists on windows but is "non blocking". So coqc would detach "coqtop -compile" and make would fail trying to step to the next target before "coqtop -compile" terminates (because coqc did terminate already).
* win32: remove outdated splash screenGravatar Enrico Tassi2014-09-17
| | | | | The official Coq logo does not work as a splash screen. Simplest fix: no splash screen.
* Fix highlighting of "Hint Unfold" and "Hint Rewrite".Gravatar Guillaume Melquiond2014-09-17
|
* Properly highlight the Export keyword.Gravatar Guillaume Melquiond2014-09-17
|
* Fix ambiguous regex in syntax highlighting.Gravatar Guillaume Melquiond2014-09-17
| | | | | | | This fix considerably speeds up syntax highlighting. It also avoids burning 100% CPU when typing long identifiers. Finally, identifiers longer than 20 characters are now properly highlighted, since the stack of the automaton no longer overflows because of them.
* Change an axiom into a definition.Gravatar Guillaume Melquiond2014-09-17
|
* Fix broken syntax highlighting for Coq files using "Proof constr".Gravatar Guillaume Melquiond2014-09-17
| | | | | | See Eqdep_dec.v for instance. Module declarations were not highlighted because the IDE wrongly believed they were used inside an unterminated proof.
* win32: bring back the coq icon in the coqide binaryGravatar Enrico Tassi2014-09-17
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 02:42:56 +0000