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.
Fix bug #3593, making constr_eq and progress work up to
equality of universes, along with a few other functions in evd.
Be more conservative and keep the use of eq_constr in pretyping/ functions.
seems to fix a looping coq-tex (when compiled with camlp4)
configure.ml: opam camlp5 + system ocaml works

I didn't understand the purpose of the previous behavior so please check this commit
fix coq_makefile