coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge PR #6946: Fix expected number of arguments for cumulative constructors.	Maxime Dénès	2018-03-09
\|\
* \	Merge PR #6949: Revert PR #873: New strategy based on open scopes for ↵	Maxime Dénès	2018-03-09
\|\ \ \| \| \| \| \| \| \| \| \|	deciding…
\| \| *	Fix expected number of arguments for cumulative constructors.	Gaëtan Gilbert	2018-03-09
\| \|/ \|/\| \| \| \| \| \| \| \| \| \| \|	We expected `nparams + nrealargs + consnrealargs` but the `nrealargs` should not be there. This breaks cumulativity of constructors for any inductive with indices (so records still work, explaining why the test case in #6747 works).
* \|	Merge PR #6775: Allow using cumulativity without forcing strict constraints.	Maxime Dénès	2018-03-09
\|\ \
\| \| *	Revert "Merge PR #873: New strategy based on open scopes for deciding which ↵	Maxime Dénès	2018-03-09
\| \|/ \|/\| \| \| \| \| \| \| \| \| \| \|	notation to use among several of them" This reverts commit 9cac9db6446b31294d2413d920db0eaa6dd5d8a6, reversing changes made to 2f679ec5235257c9fd106c26c15049e04523a307.
\| *	Delayed weak constraints for cumulative inductive types.	Gaëtan Gilbert	2018-03-09
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	When comparing 2 irrelevant universes [u] and [v] we add a "weak constraint" [UWeak(u,v)] to the UState. Then at minimization time a weak constraint between unrelated universes where one is flexible causes them to be unified.
\| *	Cumulativity: improve treatment of irrelevant universes.	Gaëtan Gilbert	2018-03-09
\| \| \| \| \| \| \| \| \| \| \| \|	In Reductionops.infer_conv we did not have enough information to properly try to unify irrelevant universes. This requires changing the Reduction.universe_compare type a bit.
\| *	Allow using cumulativity without forcing strict constraints.	Gaëtan Gilbert	2018-03-09
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Previously [fun x : Ind@{i} => x : Ind@{j}] with Ind some cumulative inductive would try to generate a constraint [i = j] and use cumulativity only if this resulted in an inconsistency. This is confusingly different from the behaviour with [Type] and means cumulativity can only be used to lift between universes related by strict inequalities. (This isn't a kernel restriction so there might be some workaround to send the kernel the right constraints, but not in a nice way.) See modified test for more details of what is now possible. Technical notes: When universe constraints were inferred by comparing the shape of terms without reduction, cumulativity was not used and so too-strict equality constraints were generated. Then in order to use cumulativity we had to make this comparison fail to fall back to full conversion. When unifiying 2 instances of a cumulative inductive type, if there are any Irrelevant universes we try to unify them if they are flexible.
* \|	Merge PR #6480: Allow Prop as source for coercions	Maxime Dénès	2018-03-09
\|\ \ \| \|/ \|/\|
* \|	Merge PR #6895: [compat] Remove "Refolding Reduction" option.	Maxime Dénès	2018-03-09
\|\ \
\| \| *	added test for coercion from type	charguer	2018-03-09
\| \| \|
\| \| *	allow Prop as source for coercions	charguer	2018-03-09
\| \|/ \|/\|
* \|	Merge PR #6945: Fix error with univ binders on monomorphic records.	Maxime Dénès	2018-03-09
\|\ \
* \ \	Merge PR #6155: Get rid of ' notation for Zpos in QArith	Maxime Dénès	2018-03-09
\|\ \ \
* \ \ \	Merge PR #6747: Relax conversion of constructors according to the pCuIC model	Maxime Dénès	2018-03-09
\|\ \ \ \
* \ \ \ \	Merge PR #6328: Fix #6313: lost goals in nested ltac in refine	Maxime Dénès	2018-03-09
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec values	Maxime Dénès	2018-03-09
\|\ \ \ \ \ \
\| \| * \| \| \| \|	More examples about shelve/given_up in tactic-in-terms.	Hugo Herbelin	2018-03-08
\| \| \| \| \| \| \|
\| \| * \| \| \| \|	Proof engine: support for nesting tactic-in-term within other tactics.	Hugo Herbelin	2018-03-08
\| \|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Tactic-in-term can be called from within a tactic itself. We have to preserve the preexisting future_goals (if called from pretyping) and we have to inform of the existence of pending goals, using future_goals which is the only way to tell it in the absence of being part of an encapsulating proofview. This fixes #6313. Conversely, future goals, created by pretyping, can call ltac:(giveup) or ltac:(shelve), and this has to be remembered. So, we do it.
* \| \| \| \| \|	Merge PR #6522: Fix core hint database issue #6521	Maxime Dénès	2018-03-08
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6816: Adding mention of shelved/given-up status in Show Existentials	Maxime Dénès	2018-03-08
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6926: An experimental 'Show Extraction' command (grant feature ↵	Maxime Dénès	2018-03-08
\|\ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	wish #4129)
\| \| \| \| \| \| \| \| *	[compat] Remove "Refolding Reduction" option.	Emilio Jesus Gallego Arias	2018-03-08
\| \|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Following up on #6791, we remove support refolding in reduction. We also update a test case that was not properly understood, see the discussion in #6895.
\| \| \| \| \| \| \| *	Fix error with univ binders on monomorphic records.	Gaëtan Gilbert	2018-03-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Since 4eb6d29d1ca7e0cc28d59d19a50adb83f7b30a2a universe binders were declared twice for all records. Since 4fcf1fa32ff395d6bd5f6ce4803eee18173c4d36 this causes an observable error for monomorphic records.
\| \| \| \| * \| \| \|	Fix SR breakage due to allowing fixpoints on non-rec values	Matthieu Sozeau	2018-03-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We limit fixpoints to Finite inductive types, so that BiFinite inductives (non-recursive records) are excluded from fixpoint construction. This is a regression in the sense that e.g. fixpoints on unit records were allowed before. Primitive records with eta-conversion are included in the BiFinite types. Fix deprecation Fix error message, the inductive type needs to be recursive for fix to work
\| \| \| \| \| * \| \|	Add test-suite file for cumulative constructors	Matthieu Sozeau	2018-03-08
\| \| \| \| \| \| \|/ \| \| \| \| \| \|/\|
* \| \| \| \| \| \|	Merge PR #6899: [compat] Remove "Standard Proposition Elimination"	Maxime Dénès	2018-03-08
\|\ \ \ \ \ \ \ \| \|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \|
* \| \| \| \| \| \|	Merge PR #6582: Mangle auto-generated names	Maxime Dénès	2018-03-08
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6903: [compat] Remove "Shrink Abstract"	Maxime Dénès	2018-03-08
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)	Maxime Dénès	2018-03-08
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj`	Maxime Dénès	2018-03-07
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #6790: Allow universe declarations for [with Definition].	Maxime Dénès	2018-03-07
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6462: Sanitize universe declaration in Context (stop using a ref...)	Maxime Dénès	2018-03-07
\|\ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| * \| \| \| \|	An experimental 'Show Extraction' command (grant feature wish #4129)	Pierre Letouzey	2018-03-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Attempt to extract the current ongoing proof (request by Clément Pit-Claudel on coqdev, and also #4129). Evars are handled as axioms.
\| \| \| \| \| * \| \| \| \| \| \| \|	[compat] Remove "Shrink Abstract"	Emilio Jesus Gallego Arias	2018-03-06
\| \|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Following up on #6791, we the option "Shrink Abstract".
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ↵	Maxime Dénès	2018-03-06
\|\ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	a record.
\| \| \| \| \| * \| \| \| \| \| \| \|	ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)	Enrico Tassi	2018-03-06
\| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6896: [compat] Remove NOOP deprecated options.	Maxime Dénès	2018-03-06
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6824: Remove deprecated options related to typeclasses.	Maxime Dénès	2018-03-06
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \| \| \|	CHANGES and tests for with Definition @{univs}	Gaëtan Gilbert	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \| \| \| \|	Sanitize universe declaration in Context (stop using a ref...)	Gaëtan Gilbert	2018-03-05
\| \| \| \| \|/ / / / / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	When there is more than one variable to declare we stop trying to attach global universes (ie monomorphic or section polymorphic) to one of them.
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6855: Update headers following #6543.	Maxime Dénès	2018-03-05
\|\ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| * \| \| \| \| \| \| \| \| \| \|	[compat] Remove NOOP and alias deprecated options.	Emilio Jesus Gallego Arias	2018-03-04
\| \| \| \| \|/ / / / / / / / / \| \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Following up on #6791, we remove: - `Record Elimination Schemes`, a deprecated alias of `Nonrecursive Elimination Schemes` - `Match Strict` a deprecated NOOP.
\| \| * / \| \| \| \| \| \| \| \| \|	Remove deprecated options related to typeclasses.	Théo Zimmermann	2018-03-04
\| \| \|/ / / / / / / / / /
\| \| \| \| * / / / / / / /	ssr: add Prenex Implicits for Some_inj to use it as a view	Anton Trunov	2018-03-04
\| \| \| \|/ / / / / / / / \| \| \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	Merge PR #935: Handling evars in the VM	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \ \ \| \|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	Merge PR #6791: Removing compatibility support for versions older than 8.5.	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6879: Fix #6878: univ undefined for [with Definition] bad instance ↵	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	size.
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #915: Fix rewrite in * side conditions	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| * \| \| \| \| \| \| \| \| \|	Removing test for bug #2850.	Pierre-Marie Pédrot	2018-03-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This test was actually checking that evar-containing terms were making the VM fail. Obviously this is not the case anymore, so the test is now invalid.