coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-08-28	In "About", print all arguments, even if it is trailing list of _.	Hugo Herbelin

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.
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.