coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Removing trivial compatibility layer in refl_omega.	Pierre-Marie Pédrot	2017-04-24
*	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\|\
\| *	Moving the Ltac plugin to a pack-based one.	Pierre-Marie Pédrot	2017-02-17
* \|	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot	2017-02-14
* \|	Reductionops now return EConstrs.	Pierre-Marie Pédrot	2017-02-14
* \|	Tactics API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Tacmach API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|/
*	Merging Stdarg and Constrarg.	Pierre-Marie Pédrot	2016-09-21
*	Reduce warning noise when compiling the standard library.	Guillaume Melquiond	2016-08-09
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Compilation via pack for plugins of the stdlib	Pierre Letouzey	2016-06-08
*	Removing "intro" from the tactic AST.	Pierre-Marie Pédrot	2016-06-03
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	Put the "generalize" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
*	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
*	Removing the special status of generic entries defined by Coq itself.	Pierre-Marie Pédrot	2016-03-17
*	Making parentheses mandatory in tactic scopes.	Pierre-Marie Pédrot	2016-03-04
*	Getting rid of the "<:tactic< ... >>" quotations.	Pierre-Marie Pédrot	2016-02-24
*	Moving conversion functions to the new tactic API.	Pierre-Marie Pédrot	2016-02-15
*	Fix some typos.	Guillaume Melquiond	2015-12-07
*	Fix some typos.	Guillaume Melquiond	2015-10-13
*	Switch the few remaining iso-latin-1 files to utf8	Pierre Letouzey	2014-12-09
*	Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.	Hugo Herbelin	2014-12-07
*	"allows to", like "allowing to", is improper	Jason Gross	2014-08-25
*	Clean up a comment in plugins/romega/ReflOmegaCore	Jason Gross	2014-08-25
*	Grammar: "allowing to" is not proper English	Jason Gross	2014-08-25
*	Reorganization of tactics:	Hugo Herbelin	2014-08-18
*	Fix semantics of change p with c to typecheck c at each specific occurrence o...	Matthieu Sozeau	2014-06-23
*	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot	2014-05-12
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack	2013-11-02
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	Turn many List.assoc into List.assoc_f	letouzey	2013-10-24
*	cList: a few alternative to hashtbl-based uniquize, distinct, subset	letouzey	2013-10-23
*	cList.index is now cList.index_f, same for index0	letouzey	2013-10-23
*	cList: set-as-list functions are now with an explicit comparison	letouzey	2013-10-23
*	Removing a bunch of generic equalities.	ppedrot	2013-09-27
*	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc	2013-09-19
*	Restrict (try...with...) to avoid catching critical exn (part 15)	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 11)	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 7)	letouzey	2013-03-13
*	Dir_path --> DirPath	letouzey	2013-02-19
*	No more constant named "int" in Coq theories (cf bug #2878)	letouzey	2012-12-18
*	Modulification of dir_path	ppedrot	2012-12-14
*	Modulification of identifier	ppedrot	2012-12-14
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	More cleaning on Utils and CList. Some parts of the code being	ppedrot	2012-09-17
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14