coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Getting rid of the Update constructor in Reductionops.	Pierre-Marie Pédrot	2017-12-06
\| \| \| \| \|	This was dead code, probably due to the fact it was once shared with the kernel stack type.
*	Getting rid of the Shift constructor in Reductionops.	Pierre-Marie Pédrot	2017-12-06
\| \| \| \| \|	It was actually not used. The only place generating one was easily writable without it.
*	Proper nametab handling of global universe names	Matthieu Sozeau	2017-12-01
\| \| \| \| \| \| \| \|	They are now bound at the library + module level and can be qualified and shadowed according to the usual rules of qualified names. Parsing and printing of universes "u+n" done as well. In sections, global universes are discharged as well, checking that they can be defined globally when they are introduced
*	Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes ↵	Maxime Dénès	2017-11-30
\|\ \| \| \| \| \| \|	#3125)
\| *	Adding a variant get_truncation_family_of of get_sort_family_of.	Hugo Herbelin	2017-11-28
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This function returns InProp or InSet for inductive types only when the inductive type has been explicitly truncated to Prop or (impredicative) Set. For instance, singleton inductive types and small (predicative) inductive types are not truncated and hence in Type.
\| *	Moving non-recursive function sort_family_of out of the retype block of ↵	Hugo Herbelin	2017-11-28
\| \| \| \| \| \| \| \|	recursive functions.
* \|	Merge PR #1033: Universe binder improvements	Maxime Dénès	2017-11-28
\|\ \
* \| \|	[api] Remove aliases of `Evar.t`	Emilio Jesus Gallego Arias	2017-11-26
\| \|/ \|/\| \| \| \| \| \| \|	There don't really bring anything, we also correct some minor nits with the printing function.
\| *	Fix interpretation of global universes in univdecl constraints.	Gaëtan Gilbert	2017-11-25
\| \| \| \| \| \| \| \|	Also nicer error when the constraints are impossible.
\| *	Use Maps and ids for universe binders	Gaëtan Gilbert	2017-11-24
\|/ \| \| \|	Before sometimes there were lists and strings.
*	Merge PR #486: Make some functions on terms more robust w.r.t new term ↵	Maxime Dénès	2017-11-24
\|\ \| \| \| \| \| \|	constructs.
\| *	Make some functions on terms more robust w.r.t new term constructs.	Maxime Dénès	2017-11-23
\| \| \| \| \| \| \| \| \| \| \| \|	Extending terms is notoriously difficult. We try to get more help from the compiler by making sure such an extension will trigger non exhaustive pattern matching warnings.
* \|	[api] A few more minor deprecation notices.	Emilio Jesus Gallego Arias	2017-11-22
\| \| \| \| \| \| \| \|	Note the problem with `create_evar_defs`.
* \|	[api] Deprecate Term destructors, move to Constr	Emilio Jesus Gallego Arias	2017-11-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	We mirror the structure of EConstr and move the destructors from `Term` to `Constr`. This is a step towards having a single module for `Constr`.
* \|	[api] Miscellaneous consolidation + moves to engine.	Emilio Jesus Gallego Arias	2017-11-21
\|/ \| \| \| \| \|	We deprecate a few functions that were deprecated in the comments plus we place `Nameops` and `Univops` in engine where they do seem to belong in the large picture of code organization.
*	Merge PR #6025: Fix #5761: cbv on undefined evars under binders produces ↵	Maxime Dénès	2017-11-20
\|\ \| \| \| \| \| \|	unbound rel
\| *	Fix #5761: cbv on undefined evars under binders produces unbound rel	Gaëtan Gilbert	2017-11-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	When an evar is undefined we need to substitute inside the evar instance. With help from @herbelin and @psteckler to identify the issue from a large test case.
* \|	[api] Another large deprecation, `Nameops`	Emilio Jesus Gallego Arias	2017-11-13
\|/
*	Merge PR #6098: [api] Move structures deprecated in the API to the core.	Maxime Dénès	2017-11-13
\|\
* \	Merge PR #6117: Fix printing anomaly in conv	Maxime Dénès	2017-11-13
\|\ \
* \ \	Merge PR #6065: [api] Deprecate all legacy uses of Names in core.	Maxime Dénès	2017-11-13
\|\ \ \
* \ \ \	Merge PR #922: New beta-iota compatibility refinements	Maxime Dénès	2017-11-08
\|\ \ \ \
\| \| \| * \|	Fixing missing separator in an error message.	Hugo Herbelin	2017-11-08
\| \|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \|	The message is the "Conversion test raised an anomaly" one.
\| \| \| *	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
\| \| \|/ \| \| \| \| \| \| \| \| \|	We do up to `Term` which is the main bulk of the changes.
\| \| *	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
\| \|/ \|/\| \| \| \| \|	This will allow to merge back `Names` with `API.Names`
* \|	Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core.	Maxime Dénès	2017-11-06
\|\ \
* \| \|	Refining PR#924 (insensitivity of projection heuristics to alphabet).	Hugo Herbelin	2017-11-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We refine the criterion for selecting a projection. Before PR#924 it was alphabetic (i.e. morally "random" up to alpha-conversion). After PR#924 it was chronological. We refine a bit more by giving priority to simple projections when they exist over projections which include an evar instantiation (and which may actually be ill-typed).
\| * \|	[api] Deprecate all legacy uses of Name.Id in core.	Emilio Jesus Gallego Arias	2017-11-04
\|/ / \| \| \| \| \| \|	This is a first step towards some of the solutions proposed in #6008.
* \|	Merge PR #6037: Fixing #5401 (printing of patterns with bound anonymous ↵	Maxime Dénès	2017-11-03
\|\ \ \| \| \| \| \| \| \| \| \|	variables).
* \ \	Merge PR #924: Fixing part of #5669: unification heuristics sensitive to ↵	Maxime Dénès	2017-11-03
\|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \|	alphabet
\| \| * \|	Fixing #5401 (printing of patterns with bound anonymous variables).	Hugo Herbelin	2017-10-28
\| \|/ / \|/\| \| \| \| \| \| \| \|	This fixes also #5731, #6035, #5364.
* \| \|	[general] Remove Econstr dependency from `intf`	Emilio Jesus Gallego Arias	2017-10-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	To this extent we factor out the relevant bits to a new file, ltac_pretype.
* \| \|	unification: fix BZ#5692, recognize prim projs as CS projections	Matthieu Sozeau	2017-10-17
\| \| \|
* \| \|	Properly handling projection parameters in canonical structures.	Pierre-Marie Pédrot	2017-10-17
\| \| \|
* \| \|	Handling primitive projections in canonical structures.	Pierre-Marie Pédrot	2017-10-17
\| \| \|
* \| \|	Merge PR #1109: Handle some misc todos	Maxime Dénès	2017-10-09
\|\ \ \
* \ \ \	Merge PR #1084: After testing it in live, writing metas using an ↵	Maxime Dénès	2017-10-03
\|\ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	?INTERNAL#42 style is ugly
\| \| * \| \|	Remove some duplication between Typeops and Nativenorm.	Gaëtan Gilbert	2017-09-29
\| \| \| \| \|
\| \| * \| \|	Remove trivial TODO comment (constants can't be template poly now).	Gaëtan Gilbert	2017-09-28
\| \| \| \| \|
* \| \| \| \|	Efficient computation of the names contained in an environment.	Pierre-Marie Pédrot	2017-09-28
\| \| \| \| \|
* \| \| \| \|	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot	2017-09-28
\| \|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The old algorithm was relying on list membership, which is O(n). This was nefarious for terms with many binders. We use instead sets in O(log n).
* \| \| \|	Merge PR #688: Binding universe constraints in Definition/Inductive/etc...	Maxime Dénès	2017-09-26
\|\ \ \ \
* \ \ \ \	Merge PR #1083: Fixing bug in building _rect scheme for inductive types with ↵	Maxime Dénès	2017-09-25
\|\ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	let-ins and non-recursively uniform parameters
* \ \ \ \ \	Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in ↵	Maxime Dénès	2017-09-25
\|\ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	4e70791).
\| \| \| \| * \| \|	After testing it in live, writing metas using an ?INTERNAL#42 style is ugly.	Hugo Herbelin	2017-09-23
\| \|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Printing metas still happens relatively often. From the user point of view, no need to know that it is different from an evar, so the notation ?M42 as it was before is much lighter. As for developers looking for debugging information, they will easily suspect that it is internally a meta because of the "M". This reverts "Proposing meta names more distinguishable from evar names than ?M42." (dc5b8f1793c6f7104f0b4762d9887be255709ead).
\| * \| \| \| \|	Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).	Hugo Herbelin	2017-09-23
\| \| \| \| \| \|
\| \| * \| \| \|	Fixing _rect bug for inductive types with let-ins and non-rec uniform params.	Hugo Herbelin	2017-09-23
\| \|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The bug was caused by an inconsistency in different part of the code for deciding where cutting the context in between recursively uniform parameters and non-recursively uniform ones when let-ins were in the middle. We fix it by using uniformly "context_chop".
* \| \| \| \|	Merge PR #1074: Fix BZ#5750 (recovering ability to print the hole of a ↵	Maxime Dénès	2017-09-22
\|\ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	context obtained by ltac pattern-matching)
\| * \| \| \| \|	Proposing meta names more distinguishable from evar names than ?M42.	Hugo Herbelin	2017-09-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Using "?INTERNAL#42" with a # to emphasize a meaningless re-parsability. Tough maybe it signals too much an unelegant debugging flavor?
\| * \| \| \| \|	A possible fix to BZ#5750 (ability to print context of ltac subterm match).	Hugo Herbelin	2017-09-21
\| \|/ / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The main fix is to use is_ident_soft. The rest of the commit is to provide something a bit more appealing than "?M-1".