coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \| \| \|	Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monad	Maxime Dénès	2018-03-05
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #935: Handling evars in the VM	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \| \|_\|_\|_\|/ / \|/\| \| \| \| \|
\| \| * \| \| \|	reductionops: remove dead code "bind_assum"	Enrico Tassi	2018-03-04
* \| \| \| \| \|	Merge PR #6791: Removing compatibility support for versions older than 8.5.	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \| \|_\|/ / / / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \
\| \| \| \| \| \| *	Pass the constant cache as a separate argument in kernel reduction.	Pierre-Marie Pédrot	2018-03-04
\| \| \| * \| \| \|	Handling evars in the VM.	Pierre-Marie Pédrot	2018-03-03
\| \| \| \| \|_\|/ \| \| \| \|/\| \|
\| \| \| \| \| *	[compat] Remove "Tactic Pattern Unification"	Emilio Jesus Gallego Arias	2018-03-03
\| \| \| \| \|/ \| \| \| \|/\|
\| \| * \| \|	Remove 8.5 compatibility support.	Théo Zimmermann	2018-03-02
\| \| * \| \|	Remove VOld compatibility flag.	Théo Zimmermann	2018-03-02
\| \| \|/ /
* \| / /	[VM] Unify Const_sorts and Const_type, and remove Vsort.	Maxime Dénès	2018-03-02
\| \|/ / \|/\| \|
\| * \|	[econstr] Continue consolidation of EConstr API under `interp`.	Emilio Jesus Gallego Arias	2018-02-28
\|/ /
* \|	comment "resolvability" bit in Evd.evar_map	Enrico Tassi	2018-02-27
\| *	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|/
*	Merge PR #6776: Fixes bug #6774 (anomaly with ill-typed template polymorphism).	Maxime Dénès	2018-02-24
\|\
* \|	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias	2018-02-22
* \|	Merge PR #6767: [ci] add elpi	Maxime Dénès	2018-02-21
\|\ \
\| \| *	Fixes bug #6774 (anomaly with ill-typed template polymorphism).	Hugo Herbelin	2018-02-20
* \| \|	Using an "as" clause when needed for printing irrefutable patterns.	Hugo Herbelin	2018-02-20
* \| \|	Adding patterns in the category of binders for notations.	Hugo Herbelin	2018-02-20
* \| \|	Canonically add an encoding in glob_constr of "as" operator for cases_pattern.	Hugo Herbelin	2018-02-20
* \| \|	Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.	Hugo Herbelin	2018-02-20
\| \|/ \|/\|
\| *	pretyping: restore API understand_judgment_tcc (now understand_tcc_ty)	Enrico Tassi	2018-02-19
\|/
*	Merge PR #6759: detype_case predicate is not optional	Maxime Dénès	2018-02-19
\|\
* \|	Cleaner treatment of parameters in inferCumulativity	Gaëtan Gilbert	2018-02-16
* \|	Fix reduction flags in inferCumulativity	Gaëtan Gilbert	2018-02-16
\| *	detype_case predicate is not optional	Gaëtan Gilbert	2018-02-14
\|/
*	Merge PR #1082: Fixing Print for inductive types with let-in in parameters	Maxime Dénès	2018-02-12
\|\
* \	Merge PR #6128: Simplification: cumulativity information is variance informa...	Maxime Dénès	2018-02-12
\|\ \
* \ \	Merge PR #6418: More detailed error messages for Canonical Structure, #6398	Maxime Dénès	2018-02-12
\|\ \ \
* \ \ \	Merge PR #6651: Use r.(p) syntax to print primitive projections.	Maxime Dénès	2018-02-12
\|\ \ \ \
\| \| \| * \|	inferCumulativity: add comment to explain [if not is_arity].	Gaëtan Gilbert	2018-02-11
\| \| \| * \|	Use specialized function for inductive subtyping inference.	Gaëtan Gilbert	2018-02-11
\| \| \| * \|	Inference of inductive subtyping does not need an evar map.	Gaëtan Gilbert	2018-02-10
\| \| \| * \|	Simplification: cumulativity information is variance information.	Gaëtan Gilbert	2018-02-10
\| \| \| * \|	[get_cumulativity_constraints] allowing further code sharing.	Gaëtan Gilbert	2018-02-10
\| \| \| * \|	Factorize code for comparing maybe-cumulative inductives.	Gaëtan Gilbert	2018-02-10
\| \| \| * \|	Fix typo in Univ.CumulativityInfo	Gaëtan Gilbert	2018-02-10
\| \|_\|/ / \|/\| \| \|
* \| \| \|	Merge PR #6686: Kernel/checker reduction cleanups around projection unfolding	Maxime Dénès	2018-02-07
\|\ \ \ \
\| \| \| * \|	More detailed error messages for Canonical Structure, #6398	Paul Steckler	2018-02-06
* \| \| \| \|	[native_compute] Fix handling of evars in conversion	Maxime Dénès	2018-02-05
* \| \| \| \|	[native_compute] Remove useless conversion to list in reification.	Maxime Dénès	2018-02-05
\| \|_\|/ / \|/\| \| \|
\| * \| \|	Reductionops.nf_* now take an environment.	Gaëtan Gilbert	2018-02-02
\|/ / /
* \| \|	Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.	Maxime Dénès	2018-01-31
\|\ \ \
\| \| * \|	Use r.(p) syntax to print primitive projections.	Maxime Dénès	2018-01-30
\| \|/ / \|/\| \|
* \| \|	Merge PR #6666: Fix reduction of primitive projections on coinductive records...	Maxime Dénès	2018-01-30
\|\ \ \
\| * \| \|	[cbv] Fix evaluation of cofixpoints under primitive projections.	Maxime Dénès	2018-01-29
* \| \| \|	Safer VM interfaces	Maxime Dénès	2018-01-26
\|/ / /
* \| \|	Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants for...	Maxime Dénès	2018-01-23
\|\ \ \
\| * \| \|	Remove dead code in Environ.	Pierre-Marie Pédrot	2018-01-20