coq - The formal proof system

Age	Commit message (Collapse)	Author
2014-03-05	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey
	The removed code isn't used locally and isn't exported in the signature
2014-02-27	Remove unsafe code (Obj.magic) in Tacinterp.	Arnaud Spiwack
	This commit also introduces a module Monad to generate monadic combinators (currently, only List.map).
2014-01-19	Adding a default object to generic argument registering mechanism.	Pierre-Marie Pédrot

2013-12-19	Removing the useless pattern ident genarg.	Pierre-Marie Pédrot

2013-12-01	Removing RefArgType generic argument.	Pierre-Marie Pédrot

2013-11-30	Getting rid of casted_open_constr. It was only used by the	Pierre-Marie Pédrot
	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.
2013-08-04	Small cleaning of printing coercion failures in Ltac interpretation.	ppedrot
	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
2013-07-05	Removing SortArgType.	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16618 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-05	Expurgating the useless difference between List0 and List1 at the	ppedrot
	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
2013-06-30	Using functors to reduce the boilerplate used in registering	ppedrot
	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
2013-06-27	Getting rid of IntroPatternArgType.	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16610 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-21	Splitted up Genarg in four different levels:	ppedrot
	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