coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey	2014-03-05
\| \| \| \|	The removed code isn't used locally and isn't exported in the signature
*	Remove unsafe code (Obj.magic) in Tacinterp.	Arnaud Spiwack	2014-02-27
\| \| \|	This commit also introduces a module Monad to generate monadic combinators (currently, only List.map).
*	Adding a default object to generic argument registering mechanism.	Pierre-Marie Pédrot	2014-01-19
\|
*	Removing the useless pattern ident genarg.	Pierre-Marie Pédrot	2013-12-19
\|
*	Removing RefArgType generic argument.	Pierre-Marie Pédrot	2013-12-01
\|
*	Getting rid of casted_open_constr. It was only used by the	Pierre-Marie Pédrot	2013-11-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	refine tactic, which now uses plain glob_constr's. Now there is no real need to depend on goal when interpreting genargs. Possible minor incompatibilities: 1. The interpretation of glob_constr to constr is now done by Goal.constr_of_raw, which may be slightly dumbier than the dedicated Tacinterp.interp_open_constr which tries harder. Stdlib and test-suite do go through, though. 2. I had to change the parsing level of wit_glob in Extraargs from lconstr to constr. It may break ML notations using glob, but as they are only used inside Coq code and all well-parenthezised, it should be OK.
*	Small cleaning of printing coercion failures in Ltac interpretation.	ppedrot	2013-08-04
\| \| \| \| \| \|	Now we at least print the type of the offending object. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16657 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removing SortArgType.	ppedrot	2013-07-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16618 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Expurgating the useless difference between List0 and List1 at the	ppedrot	2013-07-05
\| \| \| \| \| \| \| \| \| \|	level of generic arguments. This only matters at parsing time. TODO: the current status is not satisfactory enough, as rule emptyness is still decided w.r.t. generic arguments. This should be done on a grammar entry basis instead. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16617 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Using functors to reduce the boilerplate used in registering	ppedrot	2013-06-30
\| \| \| \| \| \|	generic argument stuff, including the unsafe Obj.magic-like casts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16614 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Getting rid of IntroPatternArgType.	ppedrot	2013-06-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16610 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Splitted up Genarg in four different levels:	ppedrot	2013-06-21
	1. Genarg itself which only defines the abstract datatypes needed. 2. Genintern, first file of interp/, defining the intern and subst functions. 3. Geninterp, first file of tactics/, defining the interp function. 4. Genprint, first file of printing/, dealing with the printers. The Genarg file has no dependency and is in lib/, so that we can put generic arguments everywhere, and in particular in ASTs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16601 85f007b7-540e-0410-9357-904b9bb8a0f7