aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* 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
|
* win32: use subsystem windows on windows (and not console)Gravatar Enrico Tassi2014-09-17
| | | | This makes the hammer tools/mkwinapp.ml kind of obsolete
* Revert "While resolving typeclass evars in clenv, touch only the ones that ↵Gravatar Matthieu Sozeau2014-09-17
| | | | | | | | 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.
* While resolving typeclass evars in clenv, touch only the ones that appear in theGravatar Matthieu Sozeau2014-09-17
| | | | | clenv's value and type, ensuring we don't try to solve unrelated goals (fixes bug#3633).
* Update test-suite files after last commit. Add a file for rewrite_stratGravatar Matthieu Sozeau2014-09-17
| | | | examples.
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
| | | | | | | | 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.
* Undo prints only if coqtop || emacsGravatar Enrico Tassi2014-09-16
|
* better error messageGravatar Enrico Tassi2014-09-16
|
* fix test-suite/success/decl_mode.vGravatar Enrico Tassi2014-09-16
|
* More on printing references applied to implicit arguments.Gravatar Hugo Herbelin2014-09-16
|
* Add a "Hint Mode ref (+ | -)*" hint for setting a global modeGravatar Matthieu Sozeau2014-09-15
| | | | | | | | | | | | | 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).
* Adapting ltac output test to new interpretation of binders.Gravatar Hugo Herbelin2014-09-15
|
* Fixing printing of @eq which was apparently wrong bug fixed by MS on Wed 10.Gravatar Hugo Herbelin2014-09-15
|
* Not printing goal name (reinstalled by mistake in a previous commit).Gravatar Hugo Herbelin2014-09-15
|
* Fixing line break in test for #3559.Gravatar Hugo Herbelin2014-09-15
|
* Fix timing of evar-normalisation of goals in [Ftactic.nf_enter].Gravatar Arnaud Spiwack2014-09-15
| | | | All goals were normalised up front, rather than normalised after the tactic acting on previous goal had the chance to solve some evars, which then appeared non-instantiated to tactics which do not work up to evar map (most of them).
* Ltac names in binders: some Ltac values can be seen both as terms and ↵Gravatar Arnaud Spiwack2014-09-15
| | | | | identifiers. Fixes Ergo.
* Fix: when interpreting a identifier in pretying, use the Ltac identifier ↵Gravatar Arnaud Spiwack2014-09-15
| | | | | substitution at the right place. I used to change [id] to its interpretation before calling [pretype_id]. But it's incorrect: we need to use the Ltac interpretation only when looking up the rel context (where it has been interpreted previously). It would not be to use the interpreted identifier to look up the named context or the Ltac context.
* Fix a bug in the naming of binders.Gravatar Arnaud Spiwack2014-09-15
| | | The ident closure was not propagated when pretying a [uconstr] coming from a [uconstr] closure. This bug had never been reported, as far as I'm aware.
* A small pass of code cleaning and clenv removing in Rewrite.Gravatar Pierre-Marie Pédrot2014-09-15
|
* Fixing bug #3619 in emacs mode.Gravatar Hugo Herbelin2014-09-15
|
* Avoid backtracking in typeclass search if a solution for a closedGravatar Matthieu Sozeau2014-09-15
| | | | | non-dependent or propositional constraint has already been found (same behavior as before previous patch).
* Fix bug #3610, allowing betaiotadelta reduction while unifying types ofGravatar Matthieu Sozeau2014-09-15
| | | | records in unification.ml.
* Fix bug #3621, using fold_left2 on arrays of the same size only.Gravatar Matthieu Sozeau2014-09-15
|
* Rework typeclass resolution and control of backtracking.Gravatar Matthieu Sozeau2014-09-15
| | | | | | | Add a global option to check for multiple solutions and fail in that case. Add another flag to declare classes as having unique instances (not checked but assumed correct, avoiding some backtracking).
* Removing one Evd.merge in Rewrite.Gravatar Pierre-Marie Pédrot2014-09-15
|
* More invariants in Rewrite unification.Gravatar Pierre-Marie Pédrot2014-09-15
|
* The unifying functions of Rewrite uses the return types of strategies.Gravatar Pierre-Marie Pédrot2014-09-15
|
* Splitting the uses of the unification function according to the status ofGravatar Pierre-Marie Pédrot2014-09-15
| | | | the abs flag in rewrite.
* Rewrite.apply_strategy uses the same return type as strategies.Gravatar Pierre-Marie Pédrot2014-09-14
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-16 14:52:05 +0000