coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Moving the Val module to Geninterp.	Pierre-Marie Pédrot	2016-05-04
*	Switching to an untyped toplevel representation for Ltac values.	Pierre-Marie Pédrot	2016-05-04
*	Fixing printing of toplevel values.	Pierre-Marie Pédrot	2016-04-08
*	Ensuring that the type of base generic arguments contain triples.	Pierre-Marie Pédrot	2016-03-30
*	Removing dead code in Genarg.	Pierre-Marie Pédrot	2016-03-30
*	Removing dead code in Genarg.	Pierre-Marie Pédrot	2016-03-19
*	Removing the untyped representation of genargs.	Pierre-Marie Pédrot	2016-03-19
*	Removing the registering of default values for generic arguments.	Pierre-Marie Pédrot	2016-03-17
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Moving val_cast to Tacinterp.	Pierre-Marie Pédrot	2016-01-17
* \|	Getting rid of the awkward unpack mechanism from Genarg.	Pierre-Marie Pédrot	2016-01-17
* \|	Simplification and type-safety of Pcoq thanks to GADTs in Genarg.	Pierre-Marie Pédrot	2016-01-17
* \|	Reimplementing Genarg safely.	Pierre-Marie Pédrot	2016-01-17
* \|	Temporary commit getting rid of Obj.magic unsafety for Genarg.	Pierre-Marie Pédrot	2016-01-17
* \|	Removing constr generic argument.	Pierre-Marie Pédrot	2016-01-14
* \|	Removing ident and var generic arguments.	Pierre-Marie Pédrot	2016-01-14
* \|	Removing the special status of open_constr generic argument.	Pierre-Marie Pédrot	2015-12-28
* \|	Finer-grained types for toplevel values.	Pierre-Marie Pédrot	2015-12-21
* \|	Removing ad-hoc interpretation rules for tactic notations and their genarg.	Pierre-Marie Pédrot	2015-12-21
* \|	Sharing toplevel representation for several generic types.	Pierre-Marie Pédrot	2015-12-21
* \|	Removing the now useless genarg generic argument.	Pierre-Marie Pédrot	2015-12-21
* \|	Using dynamic values in tactic evaluation.	Pierre-Marie Pédrot	2015-12-21
* \|	Attaching a dynamic argument to the toplevel type of generic arguments.	Pierre-Marie Pédrot	2015-12-21
* \|	Getting rid of some hardwired generic arguments.	Pierre-Marie Pédrot	2015-12-17
* \|	Removing dead unsafe code in Genarg.	Pierre-Marie Pédrot	2015-12-12
\|/
*	Update headers.	Maxime Dénès	2015-01-12
*	Type-safe version of genarg list / pair / opt functions.	Pierre-Marie Pédrot	2014-08-29
*	Simplification of Genarg unpackers.	Pierre-Marie Pédrot	2014-08-29
*	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey	2014-03-05
*	Remove unsafe code (Obj.magic) in Tacinterp.	Arnaud Spiwack	2014-02-27
*	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
*	Small cleaning of printing coercion failures in Ltac interpretation.	ppedrot	2013-08-04
*	Removing SortArgType.	ppedrot	2013-07-05
*	Expurgating the useless difference between List0 and List1 at the	ppedrot	2013-07-05
*	Using functors to reduce the boilerplate used in registering	ppedrot	2013-06-30
*	Getting rid of IntroPatternArgType.	ppedrot	2013-06-27
*	Splitted up Genarg in four different levels:	ppedrot	2013-06-21