coq - The formal proof system

Age	Commit message (Expand)	Author
2017-07-25	[api] Remove type equalities from API.	Emilio Jesus Gallego Arias
2017-07-17	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot
2017-06-07	Put all plugins behind an "API".	Matej Kosik
2017-06-05	Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ...	Maxime Dénès
2017-06-01	Merge PR#561: Improving the Name API	Maxime Dénès
2017-05-31	Renaming allow_patvar flag of intern_gen into pattern_mode.	Hugo Herbelin
2017-05-31	Creating a module Nameops.Name extending module Names.Name.	Hugo Herbelin
2017-05-30	Adding "epose", "eset", "eremember" which allow to set terms with	Hugo Herbelin
2017-05-30	Adding "eassert", "eenough", "epose proof", which allow to state	Hugo Herbelin
2017-05-27	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias
2017-05-25	Merge PR#608: Allow Ltac2 as a plugin	Maxime Dénès
2017-05-24	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias
2017-05-03	Allowing to pass arbitrary data in internalization environments.	Pierre-Marie Pédrot
2017-04-27	Remove some unused values and types	Gaetan Gilbert
2017-04-25	[location] [ast] Port module AST to CAst	Emilio Jesus Gallego Arias
2017-04-25	[location] [ast] Switch Constrexpr AST to an extensible node type.	Emilio Jesus Gallego Arias
2017-04-25	[location] Make location optional in Loc.located	Emilio Jesus Gallego Arias
2017-04-25	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias
2017-04-24	[location] Use located in tactics.	Emilio Jesus Gallego Arias
2017-04-24	[location] Use located in misctypes.	Emilio Jesus Gallego Arias
2017-04-24	[location] Switch glob_constr to Loc.located	Emilio Jesus Gallego Arias
2017-04-24	[location] Use Loc.located for constr_expr.	Emilio Jesus Gallego Arias
2017-03-15	Attempt to improve error message when "apply in" fail.	Hugo Herbelin
2017-03-14	Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFun	Maxime Dénès
2017-02-27	Merge PR#395: Allow hintdb to be parameters in a Ltac definition or	Maxime Dénès
2017-02-17	Ltac as a plugin.	Pierre-Marie Pédrot