coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-04-13	Simplifying the declaration of constants bound to primitive projections.	Hugo Herbelin
	We factorize code from declareInd.ml and inductiveops.ml which was already existing in record.ml. We keep expansion of local definitions in the type of fields of primitive records while these are not expanded in the non-primitive case. This is to be consistent with what Indtypes.compute_projections is doing. See discussion at #11135. We keep the unused code from inductiveops.ml for possible future use though. Include improvements contributed by Gaëtan Gilbert.
2019-08-26	Make kernel parametric on the lowest universe and fix #9294	Matthieu Sozeau
	This could be Prop (for compat with usual Coq), Set (for HoTT), or actually an arbitrary "i". Take lower bound of universes into account in pretyping/engine Reinstate proper elaboration of SProp <= l constraints: replacing is_small with equality with lbound is _not_ semantics preserving! lbound = Set Elaborate template polymorphic inductives with lower bound Prop This will make more constraints explicit Check univ constraints with Prop as lower bound for template inductives Restrict template polymorphic universes to those not bounded from below Fixes #9294 fix suggested by Matthieu Try second fix suggested by Matthieu Take care of modifying elaboration for record declarations as well. Rebase and export functions for debug Remove exported functions used while debugging Add a new typing flag "check_template" and option "-no-template-checl" This parameterizes the new criterion on template polymorphic inductives to allow bypassing it (necessary for backward compatibility). Update checker to the new typing flags structure Switch on the new template_check flag to allow old unsafe behavior in indTyping. This is the only change of code really impacting the kernel, together with the commit implementing unbounded from below and parameterization by the lower bound on universes. Add deprecated option `Unset Template Check` allowing to make proof scripts work with both 8.9 and 8.10 for a while Fix `Template Check` option name and test it Add `Unset Template Check` to Coq89.v Cooking of inductives and template-check tests Cleanup test-suite file for template check / universes(template) flags cookind tests Move test of `Unset Template Check` to the failure/ dir, but comment it for now Template test-suite test explanation Overlays for PR 9918 Overlay for paramcoq Add overlay for fiat_parsers (-no-template-check) Add overlay for fiat_crypto_legacy Update fiat-crypto legacy overlay Now it points at the version that I plan on merging; I am hoping that doing this will guard against mistakes by adding an extra check that the target tested by Coq's CI on this branch works with the change I made. Remove overlay that should no longer be necessary The setting in the compat file should handle it Remove now-merged fiat-crypto-legacy overlay Update `Print Assumptions` to reflect the typing flag for template checking Fix About and Print Assumptions for template poly, giving info on which variables are actually polymorphic Fix pretty printing to print global universe levels properly Fix printing of template polymorphic universes Fix pretty printing for template polymorphism on no universe Fix interaction of template check and universes(template) flag Fix indTyping to really check if there is any point in polymorphism: the conclusion sort should be parameterized over at least one local universe Indtyping fixes for template polymorphic Props Allow explicit template polymorphism again Adapt to new indTyping interface Handle the case of template-polymorphic on no universes correctly (morally Type0m univ represented as Prop). Fix check of meaningfullness of template polymorphism in the kernel. It is now done w.r.t the min_univ, the minimal universe inferred for the inductive/record type, independently of the user-written annotation which must only be larger than min_univ. This preserves compatibility with UniMath and template-polymorphism as it has been implemented up-to now. Comment on identity non-template-polymorphism Remove incorrect universes(template) attributes from ssr simpl_fun can be meaningfully template-poly, as well as pred_key (although the use is debatable: it could just as well be in Prop). Move `fun_of_simpl` coercion declaration out of section to respect uniform inheritance Remove incorrect uses of #[universes(template)] from the stdlib Extraction of micromega changes due to moving an ind decl out of a section Remove incorrect uses of #[universes(template)] from plugins Fix test-suite files, removing incorrect #[universes(template)] attributes Remove incorrect #[universes(template)] attributes in test-suite Fix test-suite Remove overlays as they have been merged upstream.
2019-03-30	Error when [foo.(bar)] is used with nonprojection [bar]	Gaëtan Gilbert
	(warn if bar is a nonprimitive projection)
2018-12-19	Put #[universes(template)] in outputs tests	Gaëtan Gilbert

2018-03-30	Fix #6257: anomaly with Printing Projections and Context.	Gaëtan Gilbert
	Constrextern.explicitize expected that if implicits were declared they would be declared at least up to the principal argument of the projection, but Context/discharge of implicits does not preserve this. Note the anomaly only happens with primitive projections DISABLED in recent Coqs (>=8.8). Implicit argument experts may consider whether ensuring enough implicits are declared would be better.