coq - The formal proof system

Age	Commit message (Expand)	Author
2015-10-20	Proofview.Goal.sigma returns an indexed evarmap.	Pierre-Marie Pédrot
2015-10-20	Indexing Proofview.goals with a stage.	Pierre-Marie Pédrot
2015-10-20	Boxing the Goal.enter primitive into a record type.	Pierre-Marie Pédrot
2015-10-02	Univs: fix many evar_map initializations and leaks.	Matthieu Sozeau
2015-05-13	Safer typing primitives.	Pierre-Marie Pédrot
2015-04-23	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond
2015-04-23	Using tclZEROMSG instead of tclZERO in several places.	Pierre-Marie Pédrot
2015-02-10	More expressive API for tclWITHHOLES.	Pierre-Marie Pédrot
2015-02-02	Removing dead code.	Pierre-Marie Pédrot
2015-01-12	Update headers.	Maxime Dénès
2015-01-03	Fixing #3896 (incorrect sigma given to printer).	Hugo Herbelin
2014-12-16	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot
2014-12-12	Add Ltac syntax for the [tclIFCATCH] primitive.	Arnaud Spiwack
2014-12-11	Tentatively more informative report of failure when inferring	Hugo Herbelin
2014-12-08	Constructor tactics backtracking is done using [Tacticals.New] rather than [P...	Arnaud Spiwack
2014-11-20	Adding locations to tclZEROMSG.	Pierre-Marie Pédrot
2014-11-02	Plural and singular forms in error messages.	Hugo Herbelin
2014-10-22	Proofview: split [V82] module into [Unsafe] and [V82].	Arnaud Spiwack
2014-09-08	Display number of available goals in "incorrect number of goals" error message.	Arnaud Spiwack
2014-09-06	Renaming goal-entering functions.	Pierre-Marie Pédrot
2014-08-28	Simplification of the tclCHECKINTERRUPT tactic.	Pierre-Marie Pédrot
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-18	Improving error message when applying rewrite to an expression which is not a...	Hugo Herbelin
2014-08-18	Reorganisation of intropattern code	Hugo Herbelin
2014-08-15	More self-contained code for tclWITHHOLES.	Pierre-Marie Pédrot
2014-07-13	Adding a "time" tactical for benchmarking purposes. In case the tactic	Hugo Herbelin
2014-07-10	check_for_interrupt: better (but slower) in threading mode	Enrico Tassi
2014-07-07	Revert "time tac" (committed by mistake).	Hugo Herbelin
2014-07-07	time tac	Hugo Herbelin
2014-06-24	Clenvtac.clenv_refine in the new monad. Not satisfactory though, because it	Pierre-Marie Pédrot
2014-06-23	Removing opens to Clenvtac to track its use more easily.	Pierre-Marie Pédrot
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-04-23	Removing dead code, thanks to new OCaml warnings and a bit of scripting.	Pierre-Marie Pédrot
2014-04-22	Using the new monad tactic in Inv.	Pierre-Marie Pédrot
2014-04-22	Removing tactic compatibility layer from Elim.	Pierre-Marie Pédrot
2014-04-22	Small code cleaning in Tacticals.	Pierre-Marie Pédrot
2014-04-22	Simplifying interface of elimination tactics. They used dummy clausenvs, and	Pierre-Marie Pédrot
2014-03-31	Removing the Change_evar refiner rule.	Pierre-Marie Pédrot
2014-03-26	Removing tactic compatibility layer in Equality.	Pierre-Marie Pédrot
2014-03-26	Removing Tacmach compatibility layer in Inv.	Pierre-Marie Pédrot
2014-03-26	Removing tactic compatibility layer from Inv.	Pierre-Marie Pédrot
2014-03-19	Using non-normalized goals in tactic interpretation.	Pierre-Marie Pédrot
2014-03-07	Useless tactic bindings in Tacticals.	Pierre-Marie Pédrot
2014-02-27	Proofview.Notations: Now that (>>=) is free, use it for tclBIND.	Arnaud Spiwack
2013-11-04	Fix Tacticals.New.tclREPEAT_MAiN: does not fail badly when every goal was sol...	aspiwack
2013-11-04	Fix ltac's progress tactical: requires progress in each goal.	aspiwack
2013-11-04	Fix the tactical ; [ … ] : the "incorrect number of goal" error was not cau...	aspiwack
2013-11-02	The repeat tactic now honors failure levels in ltac.	aspiwack
2013-11-02	Tacticals.New.tclWITHHOLES: clean up.	aspiwack