coq - The formal proof system

Age	Commit message (Expand)	Author
2016-06-18	Exporting a generic argument induction_arg. As a consequence,	Hugo Herbelin
2016-05-08	Removing dead code and unused opens.	Pierre-Marie Pédrot
2016-05-04	Removing useless generic arguments.	Pierre-Marie Pédrot
2016-05-04	Moving the Val module to Geninterp.	Pierre-Marie Pédrot
2016-04-27	Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"	Hugo Herbelin
2016-04-27	Revert "Revert "Honor parsing and printing levels for tactic entry in TACTIC ...	Hugo Herbelin
2016-04-27	Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"	Hugo Herbelin
2016-04-27	Honor parsing and printing levels for tactic entry in TACTIC EXTEND and	Hugo Herbelin
2016-03-20	Adding a new Ltac generic argument for forced tactics returing unit.	Pierre-Marie Pédrot
2016-03-19	Removing dead code in Genarg.	Pierre-Marie Pédrot
2016-03-17	Removing the special status of generic entries defined by Coq itself.	Pierre-Marie Pédrot
2016-03-17	Removing the registering of default values for generic arguments.	Pierre-Marie Pédrot
2016-02-22	The tactic generic argument now returns a value rather than a glob_expr.	Pierre-Marie Pédrot
2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2016-01-17	Temporary commit getting rid of Obj.magic unsafety for Genarg.	Pierre-Marie Pédrot
2016-01-14	Removing constr generic argument.	Pierre-Marie Pédrot
2016-01-14	Removing ident and var generic arguments.	Pierre-Marie Pédrot
2015-12-28	Removing the special status of open_constr generic argument.	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	Removing the now useless genarg generic argument.	Pierre-Marie Pédrot
2015-12-17	Getting rid of some hardwired generic arguments.	Pierre-Marie Pédrot
2015-03-30	grammar: export hypident	Enrico Tassi
2015-01-12	Update headers.	Maxime Dénès
2014-08-18	Lazy interpretation of patterns so that expressions such as "intros H H'/H"	Hugo Herbelin
2014-08-18	Adding a new intro-pattern for "apply in" on the fly. Using syntax	Hugo Herbelin
2014-08-05	Fix [uconstr] name for argextend.	Arnaud Spiwack
2014-07-29	Add a type of untyped term to Ltac's value.	Arnaud Spiwack
2014-04-14	Closing bug #3260	Julien Forest
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
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
2013-07-05	Removing SortArgType.	ppedrot
2013-07-02	Removing the use of leveled tactics wit_tacticn. It is now handled	ppedrot
2013-06-27	Getting rid of IntroPatternArgType.	ppedrot
2013-06-21	Cutting the dependency of Genarg in constr_expr, glob_constr	ppedrot