coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-02-14	Tactic_matching API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Eqdecide API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Class_tactics API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Eauto API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Auto API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Hints API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Leminv API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Inv API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Contradiction API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Equality API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Elim API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Tactics API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Hipattern API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Tacticals API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Clenv API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Tacmach API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Refine API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Goal API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Cleaning up opening of the EConstr module in pretyping folder.	Pierre-Marie Pédrot

2017-02-14	Making judgment type generic over the type of inner constrs.	Pierre-Marie Pédrot
	This allows to factorize code and prevents the unnecessary use of back and forth conversions between the various types of terms. Note that functions from typing may now raise errors as PretypeError rather than TypeError, because they call the proper wrapper. I think that they were wrongly calling the kernel because of an overlook of open modules.
2017-02-14	Unification API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Pretyping API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Cases API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Coercion API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Classops API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Typeclasses API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Tacred API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Constr_matching API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Patternops API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Typing API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Evarconv API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Recordops API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Evarsolve API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Evardefine API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Find_subterm API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Cbv API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Retyping API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Nativenorm API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Vnorm API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Reductionops API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Termops API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Merge PR#253: Sort Search results by relevance	Maxime Dénès

2017-02-14	Test-suite: output of Search	Arnaud Spiwack
	Fix the ordering of the results in the output of Search to correspond to the "priority" ordering.
2017-02-13	Merge PR#349: Proofview: tclINDEPENDENTL	Maxime Dénès

2017-02-10	Proofview: tclINDEPENDENTL	Enrico Tassi

2017-02-09	Turning an anomaly on 'pat into a proper "unsupported" error message.	Hugo Herbelin

2017-02-09	Fixing bug #5346 (an unimplemented application of 'pat).	Hugo Herbelin

2017-02-08	Merge PR#405: Type cleanup in `Metasyntax`	Maxime Dénès

2017-02-08	Merge PR#393: Replace Typeops with Fast_typeops	Maxime Dénès

2017-02-07	Revert "Extraction: avoid deprecated functions of module String"	Pierre Letouzey
	This reverts commit 69c4e7cfa0271f024b2178082e4be2e3ca3be263. String.capitalize_ascii are only available for ocaml >= 4.03, sorry...