coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| \| \| * \| \| \| \| \| \|	Notations: documenting structure collecting variables occurring in notation.	Hugo Herbelin	2018-02-20
\| \| \| \| * \| \| \| \| \| \|	Renaming binders into binderlists in egramcoq.ml.	Hugo Herbelin	2018-02-20
\| \| \| \| * \| \| \| \| \| \|	Introducing an intermediary type "constr_prod_entry_key" for grammar producti...	Hugo Herbelin	2018-02-20
\| \| \| \| * \| \| \| \| \| \|	Canonically add an encoding in glob_constr of "as" operator for cases_pattern.	Hugo Herbelin	2018-02-20
\| \| \| \| * \| \| \| \| \| \|	Minor clarifying of name variables in constrintern.ml.	Hugo Herbelin	2018-02-20
\| \| \| \| * \| \| \| \| \| \|	Using name given by user to name a 'pat, if any.	Hugo Herbelin	2018-02-20
\| \| \| \| * \| \| \| \| \| \|	Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.	Hugo Herbelin	2018-02-20
\| \| \| \| * \| \| \| \| \| \|	Rephrasing ETBinderList with a self-documenting and invariant-carrying argument.	Hugo Herbelin	2018-02-20
\| \| \| \| * \| \| \| \| \| \|	Notations: Do not consider a non-occurring variable as a binder-only variable.	Hugo Herbelin	2018-02-20
\| \| \| \| * \| \| \| \| \| \|	More precise explanation when a notation is not reversible for printing.	Hugo Herbelin	2018-02-20
\| \| \| \| * \| \| \| \| \| \|	Adding support for re-folding notation referring to isolated "forall '(x,y), t".	Hugo Herbelin	2018-02-20
\| \| \| \| * \| \| \| \| \| \|	Again one more step in fixing #5762 ("where" clause).	Hugo Herbelin	2018-02-20
\| \|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \|	ci: add elpi	Enrico Tassi	2018-02-19
\| \| \| \| * \| \| \| \| \|	record: restore API declare_projections (removed in e414c07e1)	Enrico Tassi	2018-02-19
\| \| \| \| * \| \| \| \| \|	pretyping: restore API understand_judgment_tcc (now understand_tcc_ty)	Enrico Tassi	2018-02-19
\| \|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #6728: Extrude monomorphic universe contexts from with Definition co...	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #6761: Remove unused argument in Record.declare_structure	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6753: [toplevel] Make toplevel state into a record.	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \| \| \| \| \|	Fix #6529: nf_evar_info and check the env evars' not just the concl	Matthieu Sozeau	2018-02-19
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6230: Better Cemitcodes API + compact relocation representation	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6759: detype_case predicate is not optional	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6772: Cleanup inferCumulativity	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6648: [tactics] make apply_type safe	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ...	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead.	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6478: [build] Fix VM dynamic linking prep in byte builds.	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6571: Fix ci-all target	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Change references to CAMLP4 to CAMLP5 to be more accurate since we no	Jim Fehrle	2018-02-17
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	apply_type: add option "typecheck" passed down to refine	Enrico Tassi	2018-02-16
\| \|_\|_\|_\|/ / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Cleaner treatment of parameters in inferCumulativity	Gaëtan Gilbert	2018-02-16
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fix reduction flags in inferCumulativity	Gaëtan Gilbert	2018-02-16
\| \|_\|_\|_\|/ / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Adding a test for the construction that was broken in Coccinelle.	Pierre-Marie Pédrot	2018-02-16
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Extrude monomorphic universe contexts from with Definition constraints.	Pierre-Marie Pédrot	2018-02-16
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Adding a test for variance subtyping in the module system.	Pierre-Marie Pédrot	2018-02-15
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Adding a sanity check on inductive variance subtyping.	Pierre-Marie Pédrot	2018-02-15
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	[toplevel] Make toplevel state into a record.	Emilio Jesus Gallego Arias	2018-02-15
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	[ide] Localize a IDE-specific flag.	Emilio Jesus Gallego Arias	2018-02-15
\| \|_\|_\|_\|_\|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #1073: new quick2vo target: like vio2vo, but smarter	Maxime Dénès	2018-02-15
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	disable tests: vio2vo is broken in Windows	Ralf Jung	2018-02-15
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	also test vio2vo	Ralf Jung	2018-02-15
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	test "make quick2vo"	Ralf Jung	2018-02-15
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	new quick2vo target: like vio2vo, but smarter	Ralf Jung	2018-02-15
\| \| \|_\|_\|/ / / / / / / / / / / / \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6741: coq_makefile: Support "" as the prefix in _CoqProject	Maxime Dénès	2018-02-15
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	coq_makefile: Support "" as the prefix in _CoqProject	Joachim Breitner	2018-02-15
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6760: CHANGES for 8.7.2.	Maxime Dénès	2018-02-15
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Extend `zify_N` with knowledge about `N.pred`	Joachim Breitner	2018-02-14
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	CHANGES for 8.7.2.	Théo Zimmermann	2018-02-14
\|/ / / / / / / / / / / / / / / /
\| \| \| \| \| \| \| \| \| * / / / / / /	Remove unused argument in Record.declare_structure	Gaëtan Gilbert	2018-02-14
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Factorize the relocations in the on-disk VM representation.	Pierre-Marie Pédrot	2018-02-14