coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Creating a dedicated ltac/ folder for Hightactics.	Pierre-Marie Pédrot	2016-03-21
\|
*	Adding a new folder corresponding to the low-level part of the pretyper	Pierre-Marie Pédrot	2015-02-27
\| \| \| \| \| \| \|	together with the tactic monad. The move is not complete yet, because some file candidates for this directory have almost useless dependencies in other ones that should not be moved.
*	Fixing include of debugger.	Pierre-Marie Pédrot	2014-08-18
\|
*	configure.ml: our configure script is now written in ML :-)	Pierre Letouzey	2013-12-20
	configure is now just a minimal wrapper around the new configure.ml. This configure.ml is runned with the same ocaml used during compilation, and starts with a #load "unix.cma". For now, this new configure script is meant to be 99% compatible with the old one. Known incompatibilities : the --foo option format (with two --) isn't supported anymore, use -foo options instead. Let me know if you encounter any other changes. Internals: - We use our own "run" command (based on Unix.create_process) to avoid relying on some specific shell (/bin/sh or cmd.exe). - We should have far less issues with filename quoting under windows since we almost never rely on (cygwin) shell anymore. This remains to be fully tested, though. - dev/ocamldebug-coq is slightly different now, to ease its generation