coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #7655: Refactor parsing rules for Hint Resolve -> and Hint Resolve <-	Pierre-Marie Pédrot	2018-06-04
\|\
* \	Merge PR #7601: Fix notation for code snippet in documentation	Maxime Dénès	2018-06-04
\|\ \
* \ \	Merge PR #7418: Actually take advantage of the normalization status of kernel...	Maxime Dénès	2018-06-04
\|\ \ \
* \ \ \	Merge PR #7199: Fixes #7195: missing freshness condition in Ltac pattern-matc...	Matthieu Sozeau	2018-06-04
\|\ \ \ \
* \ \ \ \	Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode.	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #7114: Fix #7113: Program Let Fixpoint in section causes anomaly	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #7189: Fix #5539: algebraic universe produced by cases.	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #7349: Fix an anomaly when calling Obligation 0 or Obligation -1.	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #7013: Fixes #7011: Fix/CoFix were not considered in main loop of ta...	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #7216: Replace uses of Termops.dependent by more specific functions.	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #7552: Fix #7539: Checker does not properly handle negative coinduct...	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #7590: Fix #7586: Anomaly "Uncaught exception Not_found".	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7249: Cleaning, documentation, uniformisation of the Coq extension ...	Pierre-Marie Pédrot	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7619: Mention test-suite in PR template	Maxime Dénès	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7648: Indicate in the doc that clearbody can take several idents	Maxime Dénès	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7496: Fix #4403: insufficient handling of type-in-type in kernel.	Maxime Dénès	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7657: Fix a couple typos in deprecation messages	Pierre-Marie Pédrot	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7640: Small refactoring to clarify make_local_hint_db.	Pierre-Marie Pédrot	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7649: Remove some dead code in class_tactics.ml	Pierre-Marie Pédrot	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7682: Fixes #7641: more detailed message about disjunctive patterns...	Emilio Jesus Gallego Arias	2018-06-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7689: configure: fix warning printing	Emilio Jesus Gallego Arias	2018-06-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7637: Fix an outdated comment refering to lib/dnet.mli	Pierre-Marie Pédrot	2018-06-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	configure: fix warning printing	Gaëtan Gilbert	2018-06-03
\| \|/ / / / / / / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Further sharing in CList.	Hugo Herbelin	2018-06-03
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Cleaning, documentation, uniformisation of the Coq extension of List.	Hugo Herbelin	2018-06-03
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7683: [lib] Fix wrong deprecation annotations.	Pierre-Marie Pédrot	2018-06-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fixes #7641: more detailed message for disjunctive patterns with different vars.	Hugo Herbelin	2018-06-03
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7656: CI for QuickChick and ext-lib	Emilio Jesus Gallego Arias	2018-06-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Update .gitlab to use newer ocaml	Leonidas Lampropoulos	2018-06-02
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[lib] Fix wrong deprecation annotations.	Emilio Jesus Gallego Arias	2018-06-03
\| \|/ / / / / / / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7681: Fixes #7636: location missing on deprecated compatibility not...	Emilio Jesus Gallego Arias	2018-06-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	QuickChick CI	Leonidas Lampropoulos	2018-06-02
\| \|/ / / / / / / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7680: [ci] Expose updated `OCAMLPATH` for CI users.	Gaëtan Gilbert	2018-06-02
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|/ / / / / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fixes #7636: location missing on deprecated compatibility notations.	Hugo Herbelin	2018-06-02
\| \|/ / / / / / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[ci] Expose updated `OCAMLPATH` for CI users.	Emilio Jesus Gallego Arias	2018-06-02
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7234: Reduce circular dependency constants <-> projections	Maxime Dénès	2018-06-01
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|/ / / / / / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7570: [api] Move `Constrexpr` to the `interp` module.	Maxime Dénès	2018-06-01
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7537: Improve the Gallina chapter of the reference manual.	Maxime Dénès	2018-06-01
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7606: Allow more than one signature and name per Sphinx object	Maxime Dénès	2018-06-01
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7660: Add codeowner for timing python scripts	Maxime Dénès	2018-06-01
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge two clearbody docs	Théo Winterhalter	2018-06-01
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7652: Explicitly require python2 in python scripts in tools/	Jason Gross	2018-05-31
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Add codeowner for timing python scripts	Jason Gross	2018-05-31
\| \|/ / / / / / / / / / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fix a couple typos in deprecation messages	Armaël Guéneau	2018-05-31
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7401: Automatically run alienclean before compiling.	Enrico Tassi	2018-05-31
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Explicitly require python2 in python scripts in tools/	Armaël Guéneau	2018-05-31
\| \|/ / / / / / / / / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Remove some dead code in class_tactics.ml	Armaël Guéneau	2018-05-31
\| \|_\|_\|_\|_\|_\|/ / / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Refactor parsing rules for Hint Resolve -> and Hint Resolve <-	Armaël Guéneau	2018-05-31
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[notations] Split interpretation and parsing of notations	Emilio Jesus Gallego Arias	2018-05-31
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[api] Move `Constrexpr` to the `interp` module.	Emilio Jesus Gallego Arias	2018-05-31
\| \|_\|_\|/ / / / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|