fix test-suite/success/decl_mode.v
better error message
Undo prints only if coqtop || emacs
Revert specific syntax for primitive projections, avoiding ugly
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.
Update test-suite files after last commit. Add a file for rewrite_strat
examples.
While resolving typeclass evars in clenv, touch only the ones that appear in the
clenv's value and type, ensuring we don't try to solve unrelated
goals (fixes bug#3633).
Revert "While resolving typeclass evars in clenv, touch only the ones that 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.
win32: use subsystem windows on windows (and not console)

This makes the hammer tools/mkwinapp.ml kind of obsolete
win32: bring back the coq icon in the coqide binary
Fix broken syntax highlighting for Coq files using "Proof constr".

See Eqdep_dec.v for instance. Module declarations were not highlighted
because the IDE wrongly believed they were used inside an unterminated
proof.
Change an axiom into a definition.
Fix ambiguous regex in syntax highlighting.

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.
Properly highlight the Export keyword.
Fix highlighting of "Hint Unfold" and "Hint Rewrite".
win32: remove outdated splash screen

The official Coq logo does not work as a splash screen.
Simplest fix: no splash screen.
Revert "coqc: execvp is now available even on win32"

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).
Remove pointless regex for '""' as the empty string already matches it.
Add some missing Proof statements.
Change some Defined into Qed.
Fix bug #3633 properly, by delaying the interpetation of constrs in
apply f, g,... so that apply f, g. succeeds when apply f; apply g
does. It just mimicks the behavior of rewrite foo bar.