coq - The formal proof system

Age	Commit message (Expand)	Author
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-06	[uconstr]: use a closure instead of eager substitution.	Arnaud Spiwack
2014-07-29	Add a type of untyped term to Ltac's value.	Arnaud Spiwack
2014-05-22	Removing useless use of metaids in tactic AST.	Pierre-Marie Pédrot
2014-04-14	Closing bug #3260	Julien Forest
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
2014-03-02	Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code	Pierre Letouzey
2013-12-19	Removing the useless pattern ident genarg.	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-02	Removing the use of leveled tactics wit_tacticn. It is now handled	ppedrot
2013-06-21	Cutting the dependency of Genarg in constr_expr, glob_constr	ppedrot