coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Change QuestionMark for better record field missing error message.	Siddharth Bhat	2018-07-17
*	Fix #5719: Uncaught exception Invalid_argument.	Pierre-Marie Pédrot	2018-06-21
*	Better elaboration of pattern-matchings on primitive projections	Matthieu Sozeau	2018-06-15
*	Fix deprecation warning introduced by PR 664 merge	Matthieu Sozeau	2018-06-14
*	Merge PR #664: Fixing #5500 (missing test in return clause of match leading t...	Matthieu Sozeau	2018-06-14
\|\
* \|	[api] Misctypes removal: several moves:	Emilio Jesus Gallego Arias	2018-06-12
* \|	Merge PR #7189: Fix #5539: algebraic universe produced by cases.	Matthieu Sozeau	2018-06-04
\|\ \
* \ \	Merge PR #7216: Replace uses of Termops.dependent by more specific functions.	Matthieu Sozeau	2018-06-04
\|\ \ \
* \| \| \|	Use evd_combX in Cases.	Gaëtan Gilbert	2018-05-14
* \| \| \|	Deprecate Evarconv.e_conv,e_cumul	Gaëtan Gilbert	2018-05-11
* \| \| \|	Deprecate most evarutil evdref functions	Gaëtan Gilbert	2018-05-11
* \| \| \|	Evar maps contain econstrs.	Gaëtan Gilbert	2018-04-13
\| * \| \|	Replace uses of Termops.dependent by more specific functions.	Pierre-Marie Pédrot	2018-04-10
\| \| * \|	Fix #5539: algebraic universe produced by cases.	Gaëtan Gilbert	2018-04-06
\| \|/ /
* / /	[econstr] Forbid calling `to_constr` in open terms.	Emilio Jesus Gallego Arias	2018-03-31
\|/ /
\| *	Fixing #5547 (typability of return predicate in nested pattern-matching).	Hugo Herbelin	2018-03-27
* \|	Slightly refining some error messages about unresolvable evars.	Hugo Herbelin	2018-03-24
\|/
*	[located] More work towards using CAst.t	Emilio Jesus Gallego Arias	2018-03-09
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.	Hugo Herbelin	2018-02-20
*	Reductionops.nf_* now take an environment.	Gaëtan Gilbert	2018-02-02
*	Removing cumbersome location in multiple patterns.	Hugo Herbelin	2017-12-12
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	[general] Remove Econstr dependency from `intf`	Emilio Jesus Gallego Arias	2017-10-25
*	Efficient computation of the names contained in an environment.	Pierre-Marie Pédrot	2017-09-28
*	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot	2017-09-28
*	Making detyping potentially lazy.	Pierre-Marie Pédrot	2017-09-04
*	Merge PR #980: Adding combinators + a canonical renaming in List, Option, Name	Maxime Dénès	2017-08-31
\|\
\| *	Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_map	Hugo Herbelin	2017-08-29
* \|	Program: fix BZ#5683, missing lift when building case predicate	Matthieu Sozeau	2017-08-24
\|/
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	A fix to #5414 (ident bound by ltac names now known for "match").	Hugo Herbelin	2017-06-09
*	Remove the Sigma (monotonous state) API.	Maxime Dénès	2017-06-06
*	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
*	Merge PR#696: Trunk+cleanup constr of global	Maxime Dénès	2017-06-01
\|\
* \	Merge PR#561: Improving the Name API	Maxime Dénès	2017-06-01
\|\ \
\| * \|	Creating a module Nameops.Name extending module Names.Name.	Hugo Herbelin	2017-05-31
* \| \|	Support for using type information to infer more precise evar sources.	Hugo Herbelin	2017-05-30
\|/ /
\| *	Pretyping cleanup: remove constr_of_global calls	Matthieu Sozeau	2017-05-29
\|/
*	[coqlib] Move `Coqlib` to `library/`.	Emilio Jesus Gallego Arias	2017-05-27
*	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\
\| *	A refined solution to the beta-iota discrepancies between 8.4 and 8.5 "refine".	Hugo Herbelin	2017-04-27
* \|	[location] [ast] Port module AST to CAst	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-25
* \|	[location] Switch glob_constr to Loc.located	Emilio Jesus Gallego Arias	2017-04-24
* \|	[location] Move Glob_term.predicate_pattern to located.	Emilio Jesus Gallego Arias	2017-04-24
* \|	[location] Move Glob_term.cases_pattern to located.	Emilio Jesus Gallego Arias	2017-04-24
\|/
*	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-04-15
\|\
\| *	Fixing #5460 (limitation in computing deps in pattern-matching compilation).	Hugo Herbelin	2017-04-08