coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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 ↵	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	tactic unification.
* \ \ \ \ \	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 ↵	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	coinductive types.
* \ \ \ \ \ \ \	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
\|\ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	of List
* \ \ \ \ \ \ \ \ \	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 ↵	Emilio Jesus Gallego Arias	2018-06-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	patterns with different variables
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	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
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Still some discrepancies though. E.g.: - some functions taking an equality as arguments have suffix `_f` but not all; - the functions possibly raising an error have still different kinds of failure (Failure, Invalid_argument, Not_found or IndexOutOfRange, and when in the first two cases, with no unique rules in the style of the associated string - we thus avoid to document the exact string used). There are a few semantics changes: - skipn_at_least now raises a `Failure` if its argument is negative; - map3 raises an Invalid_argument "List.map3" rather than Invalid_argument "map3" and similarly for map4 - internally, map3 and map4 are now tail-recursive (by uniformity); - internally, split3 and combine3 are now tail-recursive (by uniformity); - filter is now "smart" by default and smartfilter is deprecated; - smartmap is now tail-recursive by default.
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Could still be made more detailed with more time.
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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
\| \|/ / / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Introduced in #7177
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7681: Fixes #7636: location missing on deprecated compatibility ↵	Emilio Jesus Gallego Arias	2018-06-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	notations.
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is needed for CI packages that use `META.coq` such as in https://github.com/coq/coq/pull/7656 .
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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
\| \|_\|_\|_\|_\|_\|/ / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[notations] Split interpretation and parsing of notations	Emilio Jesus Gallego Arias	2018-05-31
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Previously to this patch, `Notation_term` contained information about both parsing and notation interpretation. We split notation grammar to a file `parsing/notation_gram` as to make `interp/` not to depend on some parsing structures such as entries.
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[api] Move `Constrexpr` to the `interp` module.	Emilio Jesus Gallego Arias	2018-05-31
\| \|_\|_\|/ / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Continuing the interface cleanup we place `Constrexpr` in the internalization module, which is the one that eliminates it. This slims down `pretyping` considerably, including removing the `Univdecls` module which existed only due to bad dependency ordering in the first place. Thanks to @ Skyskimmer we also remove a duplicate `univ_decl` definition among `Misctypes` and `UState`. This is mostly a proof of concept yet as it depends on quite a few patches of the tree. For sure some tweaks will be necessary, but it should be good for review now. IMO the tree is now in a state where we can could easy eliminate more than 10 modules without any impact, IMHO this is a net saving API-wise and would help people to understand the structure of the code better.
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6969: [api] Remove functions deprecated in 8.8	Maxime Dénès	2018-05-31
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	Indicate in the doc that clearbody can take several idents	Théo Winterhalter	2018-05-31
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7564: Move interning the [hint_pattern] outside the Typeclasses hooks.	Emilio Jesus Gallego Arias	2018-05-31
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Reduce circular dependency constants <-> projections	Gaëtan Gilbert	2018-05-31
\| \|_\|_\|_\|_\|/ / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Instead of having the projection data in the constant data we have it independently in the environment.
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7578: Allow make clean to work on a fresh clone	Enrico Tassi	2018-05-31
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \