coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| \| \| \| \| \| \| \| \| \| \| \| \| * \|	test suite: make target to regenerate failing output tests	Gaëtan Gilbert	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Documenting the API change.	Pierre-Marie Pédrot	2018-06-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Adding an overlay for the Equations plugin.	Pierre-Marie Pédrot	2018-06-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Stronger invariants in unification signature.	Pierre-Marie Pédrot	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Documenting the deprecation.	Pierre-Marie Pédrot	2018-06-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Deprecate implicit tactic solving.	Pierre-Marie Pédrot	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Fixing typos in file Berardi.v	Hugo Herbelin	2018-06-03
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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
\| \|/ / / / / / / / / / / / / / / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Refuse to parse empty [Context] command.	Gaëtan Gilbert	2018-06-02
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[ci] Expose updated `OCAMLPATH` for CI users.	Emilio Jesus Gallego Arias	2018-06-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	[appveyor] Use OCaml version 4.06.1 in the Windows build.	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