coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	ROmega : O_STATE turned into a O_SUM	Pierre Letouzey	2017-05-22
*	ROmega: less contructors in the final omega trace	Pierre Letouzey	2017-05-22
*	ROmega : merge O_CONSTANT* into a single O_BAD_CONSTANT	Pierre Letouzey	2017-05-22
*	romega: add a tactic named unsafe_romega (for debugging, or bold users)	Pierre Letouzey	2017-05-22
*	romega: no more normalization trace, replaced by some Coq-side computation	Pierre Letouzey	2017-05-22
*	romega: use N instead of nat for Tvar	Pierre Letouzey	2017-05-22
*	romega: shorter trace (no more term lengths)	Pierre Letouzey	2017-05-22
*	refl_omega: refactoring of normalize_equation	Pierre Letouzey	2017-05-22
*	refl_omega: comment the lack of lifts when dealing with arrows	Pierre Letouzey	2017-05-22
*	romega: discard constructor D_mono (shorter trace + fix a bug)	Pierre Letouzey	2017-05-22
*	refl_omega: more refactoring (e.g. IntSets instead of sorted lists)	Pierre Letouzey	2017-05-22
*	refl_omega: refactoring (e.g. useless args in destructurate_pos_hyp)	Pierre Letouzey	2017-05-22
*	Removing trivial compatibility layer in refl_omega.	Pierre-Marie Pédrot	2017-04-24
*	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot	2017-02-14
*	Tactics API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	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
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	Put the "generalize" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
*	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
*	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
*	Turn many List.assoc into List.assoc_f	letouzey	2013-10-24
*	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
*	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
*	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
*	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia	2012-09-14
*	Cleaning Pp.ppnl use	ppedrot	2012-06-01
*	Noise for nothing	pboutill	2012-03-02
*	Refl_omega: replaced generic = on constr by eq_constr	puech	2011-07-29
*	Refl_omega: replaced some generic = on constr by eq_constr	puech	2011-07-29
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey	2009-03-20