Do not forget to build the unicode libraries, necessary to compile and launch coqtop in utf mode.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15743 85f007b7-540e-0410-9357-904b9bb8a0f7
Port from 8.4 branch some build fixes concerning win32 :

 r15722:
   - CAMLBIN was cygwin-specific, leading to issues with coqmktop
   - A missing Filename.quote on the temp file used in coqmktop
   - Try to shorten the cmdline passed to Sys.command in coqmktop:
     way too many includes were passed to coqmktop -boot

 r15724: Coqmktop: the +compiler-libs for ocaml4 is back
 r15725: Coqmktop: better detection of ocaml 4 and above
 r15739: ocamlbuild : a missing include for camlp4

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15744 85f007b7-540e-0410-9357-904b9bb8a0f7
Simpler configure: gcc via ocamlc, no ranlib (done by ocamlmklib)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15745 85f007b7-540e-0410-9357-904b9bb8a0f7
Extraction: document Separate Extraction and KeepSingleton

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15746 85f007b7-540e-0410-9357-904b9bb8a0f7
configure: no more need for ocamlmktop

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15747 85f007b7-540e-0410-9357-904b9bb8a0f7
configure: get rid of the -src option and of ${COQSRC}

 The -src option was antic and probably broken (many references
 to source files without the $COQRSC prefix). Instead, it's quite
 simpler to refer to paths in relative way (and safer in win32
 where the base path may include spaces and other horrors).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15748 85f007b7-540e-0410-9357-904b9bb8a0f7
Configure + Makefile : simplification when -local

 When local=true:

 - "make install" is now a no-op
 - In configure, no need hence to fill the various variables
   about installation (BINDIR, COQLIBINSTALL, MANDIR,
   DOCDIR, EMACSLIB). This avoids many references to
   absolute location of the coq sources (which may contain
   blanks or other strange chars in win32).
 - For the moment, we keep CONFIGDIR and DATADIR, used when
   launching coqide from inside the build directory.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15749 85f007b7-540e-0410-9357-904b9bb8a0f7
Revert "when cross-compiling with mingw32, let's fix the Filename.dir_sep"

This was merely cosmetic after all, since recent Windows versions
do tolerate paths with /.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15750 85f007b7-540e-0410-9357-904b9bb8a0f7
No need anymore to refer to COQLIB in ocamldebug-coq

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15751 85f007b7-540e-0410-9357-904b9bb8a0f7
No more coqtop.opt, produce directly a coqtop binary

 We now always produce two binaries, coqtop and coqtop.byte :
 - If ocamlopt is available, coqtop is directly what used to be coqtop.opt,
   no more symlinks needed.
 - Otherwise, coqtop is a copy of coqtop.byte.

 The same for coqchk and coqide...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15752 85f007b7-540e-0410-9357-904b9bb8a0f7
No more states/initial.coq, instead coqtop now requires Prelude.vo

 For starting a bare coqtop, the recommended option is now "-noinit"
 that skips the load of Prelude.vo. Option "-nois" is kept for
 compatibility, it is now an alias to "-noinit".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15753 85f007b7-540e-0410-9357-904b9bb8a0f7
myocamlbuild : fixes for new printing directory + sourceview for coqide

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15754 85f007b7-540e-0410-9357-904b9bb8a0f7
Remove a script unused since 2006 (cf commit r8626)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15755 85f007b7-540e-0410-9357-904b9bb8a0f7
CHANGES: document the end of states/initial.coq and coqtop.opt

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15756 85f007b7-540e-0410-9357-904b9bb8a0f7
test-suite: Local Tactic Notation is now legal since r15731

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15757 85f007b7-540e-0410-9357-904b9bb8a0f7
Correcting a comment in pattern-matching compilation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15758 85f007b7-540e-0410-9357-904b9bb8a0f7
Modification of the unjustified tag.

It seemed to intrusive to have it display the text underlined and red.
The goal of this tag is to notify the user when Coq doesn't guarantee
correctness, not to make the command look like an error.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15759 85f007b7-540e-0410-9357-904b9bb8a0f7
Assumption commands are now displayed as unsafe in Coqide.

They are still marked as safe if they are part of a module type, though.
Also local assumptions such as "Hypothesis" or "Context" are displayed
as unsafe if they happen to be defined without a section.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15760 85f007b7-540e-0410-9357-904b9bb8a0f7
Better highlighting of strings in coqide.

Strings were not highlighted out of comments. This would lead to funny
result, like certain strings (i.e. "(*") to cause all following code to be
highlighted as a string.

I've added strings in three different contexts (the same where comments
are highlighted). I think it's safe to do, I don't know if it's the best way,
though. In particular I don't know if it's the best way to highlight notations.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15761 85f007b7-540e-0410-9357-904b9bb8a0f7
Add option Set/Unset Extraction Conservative Types.

Extracted code need not preserve typing relations (e:t) from the source code.
This may be a problem as the extracted code may not implement the intented
interface. This option disables the optimisations which would prevent an
extracted term's type to be its extracted source term's type.

At this point the only such optimization is (I think) removing some dummy
λ-abstractions in constant definitions.

Extraction Implicit is still honored in this mode, and it's mostly necessary
to produce reasonable types. So in the conservative type mode, which
abstractions can be removed and which can'tt is entirely under the user's
control.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15762 85f007b7-540e-0410-9357-904b9bb8a0f7