coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Final part of moving Program code inside the main code. Adapted ↵	msozeau	2012-03-14
\| \| \| \| \| \|	add_definition/fixpoint and parsing of the "Program" prefix. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15036 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Noise for nothing	pboutill	2012-03-02
\| \| \| \| \| \| \| \| \| \| \|	Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix camlp4 compilation	pboutill	2012-01-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14951 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Another quick hack that works this time, to handle printing of locality in ↵	ppedrot	2012-01-23
\| \| \| \| \| \|	Program subtac. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14939 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reverted previous commit, which broke library compilation.	ppedrot	2012-01-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14925 85f007b7-540e-0410-9357-904b9bb8a0f7
*	This is a quick hack to permit the parsing of the locality flag in the ↵	ppedrot	2012-01-20
\| \| \| \| \| \|	Program subtactic. Ideally, locality flags should be handled in a nicer way... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14924 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed the pretty-printing of the Program plugin.	ppedrot	2012-01-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14917 85f007b7-540e-0410-9357-904b9bb8a0f7
*	A new mechanism to handle errors.	aspiwack	2011-05-13
\| \| \| \| \| \| \|	Instead of the monolitic Cerrors, I introduce a lightweight Errors module whose error message can be expanded by module introducing exceptions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14119 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13744 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).	herbelin	2010-07-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13311 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add (almost) compatibility with camlp4, without breaking support for camlp5	letouzey	2010-05-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The choice between camlp4/5 is done during configure with flags -usecamlp5 (default for the moment) vs. -usecamlp4. Currently, to have a full camlp4 compatibility, you need to change all "EXTEND" and "GEXTEND Gram" into "EXTEND Gram", and change "EOI" into "`EOI" in grammar entries. I've a sed script that does that (actually the converse), but I prefer to re-think it and check a few things before branching this sed into the build mechanism. lib/compat.ml4 is heavily used to hide incompatibilities between camlp4/5 and try to propose a common interface (cf LexerSig / GrammarSig). A few incompatible quotations have been turned into underlying code manually, in order to make the IFDEF CAMLP5 THEN ... ELSE ... END parsable by both camlp4 and 5. See in particular the fate of <:str_item< declare ... end >> Stdpp isn't used anymore, but rather Ploc (hidden behind local module Loc). This forces to use camlp5 > 5.01. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13019 85f007b7-540e-0410-9357-904b9bb8a0f7
*	static (and shared) camlp4use instead of per-file declaration	letouzey	2010-05-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13016 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
\| \| \| \| \| \| \| \| \| \| \|	- Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add a generic tactic option builder. Use it in firstorder to set the	msozeau	2010-03-05
\| \| \| \| \| \| \| \| \|	default solver (using "Set Firstorder Solver") and for program's obligation tactic. I don't understand exactly the reason of the warning when building states/initial.coq, anyone? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12842 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add [Next Obligation with tactic] support (wish #1953).	msozeau	2010-01-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12691 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Show Obligation Tactic	msozeau	2010-01-14
\| \| \| \| \| \| \|	- fix bug #1952. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12668 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Support "Local Obligation Tactic" (now the default in sections).	msozeau	2010-01-11
\| \| \| \| \| \| \| \|	Update Numbers that was implicitely using [simpl_relation] instead of the default tactic [program_simpl]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12647 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Stop using [obligation_tactic] from Program.Tactics as the default	msozeau	2009-09-15
\| \| \| \| \| \| \| \|	obligation tactic so that [Program] can work without importing anything. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12330 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Hack to correctly get ill-formed rec body exceptions even	msozeau	2009-09-02
\| \| \| \| \| \| \| \| \| \| \|	when the environment is reset. Bug is due to the use of the imperative the_globrevtab when trying to pretty-print the terms involved which may refer to the last defined obligation which is defined in the exception's environment and not the global one anymore. Bug reported by Francois Pottier. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12302 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵	letouzey	2009-03-20
	user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7