| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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. | |||
| 2014-09-17 | Change some Defined into Qed. | Guillaume Melquiond | |
| 2014-09-17 | Add some missing Proof statements. | Guillaume Melquiond | |
| 2014-09-17 | Remove pointless regex for '""' as the empty string already matches it. | Guillaume Melquiond | |
| 2014-09-17 | Revert "coqc: execvp is now available even on win32" | Enrico Tassi | |
| 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). | |||
| 2014-09-17 | win32: remove outdated splash screen | Enrico Tassi | |
| The official Coq logo does not work as a splash screen. Simplest fix: no splash screen. | |||
| 2014-09-17 | Fix highlighting of "Hint Unfold" and "Hint Rewrite". | Guillaume Melquiond | |
| 2014-09-17 | Properly highlight the Export keyword. | Guillaume Melquiond | |
| 2014-09-17 | Fix ambiguous regex in syntax highlighting. | Guillaume Melquiond | |
| 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. | |||
| 2014-09-17 | Change an axiom into a definition. | Guillaume Melquiond | |
| 2014-09-17 | Fix broken syntax highlighting for Coq files using "Proof constr". | Guillaume Melquiond | |
| See Eqdep_dec.v for instance. Module declarations were not highlighted because the IDE wrongly believed they were used inside an unterminated proof. | |||
| 2014-09-17 | win32: bring back the coq icon in the coqide binary | Enrico Tassi | |
| 2014-09-17 | win32: use subsystem windows on windows (and not console) | Enrico Tassi | |
| This makes the hammer tools/mkwinapp.ml kind of obsolete | |||
| 2014-09-17 | Revert "While resolving typeclass evars in clenv, touch only the ones that ↵ | Matthieu Sozeau | |
| appear in the" This reverts commit 9de1edd730eeb3cada742a27a36bc70178eda6d8. Not the right way to do it. The evd shouldn't contain unrelated evars in the first place. | |||
| 2014-09-17 | While resolving typeclass evars in clenv, touch only the ones that appear in the | Matthieu Sozeau | |
| clenv's value and type, ensuring we don't try to solve unrelated goals (fixes bug#3633). | |||
| 2014-09-17 | Update test-suite files after last commit. Add a file for rewrite_strat | Matthieu Sozeau | |
| examples. | |||
| 2014-09-17 | Revert specific syntax for primitive projections, avoiding ugly | Matthieu Sozeau | |
| contortions in internalization/externalization. It uses a fully typed version of detyping, requiring the environment, to move from primitive projection applications to regular applications of the eta-expanded version. The kernel is unchanged, and only constrMatching needs compatibility code now. | |||
| 2014-09-16 | Undo prints only if coqtop || emacs | Enrico Tassi | |
| 2014-09-16 | better error message | Enrico Tassi | |
| 2014-09-16 | fix test-suite/success/decl_mode.v | Enrico Tassi | |
| 2014-09-16 | More on printing references applied to implicit arguments. | Hugo Herbelin | |
| 2014-09-15 | Add a "Hint Mode ref (+ | -)*" hint for setting a global mode | Matthieu Sozeau | |
| of resulution for goals whose head is "ref". + means the argument is an input and shouldn't contain an evar, otherwise resolution fails. This generalizes the Typeclasses Strict Resolution option which prevents resolution to fire on underconstrained typeclass constraints, now the criterion can be applied to specific parameters. Also cleanup auto/eauto code, uncovering a potential backwards compatibility issue: in cases the goal contains existentials, we never use the discrimination net in auto/eauto. We should try to set this on once the contribs are stabilized (the stdlib goes through when the dnet is used in these cases). | |||
| 2014-09-15 | Adapting ltac output test to new interpretation of binders. | Hugo Herbelin | |
| 2014-09-15 | Fixing printing of @eq which was apparently wrong bug fixed by MS on Wed 10. | Hugo Herbelin | |
| 2014-09-15 | Not printing goal name (reinstalled by mistake in a previous commit). | Hugo Herbelin | |
| 2014-09-15 | Fixing line break in test for #3559. | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |