coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge branch 'master' into econstr	Pierre-Marie Pédrot	2017-04-07
\|\
* \|	Restore a fast path in EConstr instance normalization.	Pierre-Marie Pédrot	2017-04-01
\| \|
* \|	Using delayed universe instances in EConstr.	Pierre-Marie Pédrot	2017-04-01
\| \| \| \| \| \| \| \| \| \| \| \|	The transition has been done a bit brutally. I think we can still save a lot of useless normalizations here and there by providing the right API in EConstr. Nonetheless, this is a first step.
* \|	Actually exporting delayed universes in the EConstr implementation.	Pierre-Marie Pédrot	2017-04-01
\| \| \| \| \| \| \| \| \| \|	For now we only normalize sorts, and we leave instances for the next commit.
* \|	Make the Constr.kind_of_term type parametric in sorts and universes.	Pierre-Marie Pédrot	2017-03-31
\| \|
* \|	Ensuring proper cast invariants in EConstr.kind.	Pierre-Marie Pédrot	2017-03-31
\| \| \| \| \| \| \| \| \| \| \| \|	The kernel does fishy things with casts, such that ensuring there are no two consecutive VMcast or NATIVEcast in terms. We enforce this in EConstr view as well.
* \|	Revert "Specially crafted EConstr.kind to be more efficient."	Pierre-Marie Pédrot	2017-03-31
\| \| \| \| \| \| \| \| \| \|	This reverts commit b5f07be9fdcd41fdaf73503e5214e766bf6a303b. The performance difference was not conclusive enough to pay for the code ugliness.
* \|	Specially crafted EConstr.kind to be more efficient.	Pierre-Marie Pédrot	2017-03-30
\| \| \| \| \| \| \| \| \| \|	We do one step of loop unrolling, limit the number of allocations and mark the function as inline.
* \|	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\|\ \
\| \| *	Ensuring static invariants about handling of pending evars in Pretyping.	Pierre-Marie Pédrot	2017-03-23
\| \|/ \| \| \| \| \| \| \| \| \| \|	All functions where actually called with the second argument of the pending problem being the current evar map. We simply remove this useless and error-prone second component.
\| *	[pp] Remove uses of expensive string_of_ppcmds.	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	In general we want to avoid this as much as we can, as it will need to make choices regarding the output backend (width, etc...) and it is expensive. It is better to serve the printing backends the pretty print document itself.
* \|	Merge branch 'master'.	Pierre-Marie Pédrot	2017-02-14
\|\\|
* \|	Missing API in EConstr.	Enrico Tassi	2017-02-14
\| \|
* \|	Moving evar-normalization functions to EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \| \| \| \| \| \| \|	This removes code duplication between Evarutil and EConstr.
* \|	Namegen primitives now apply on evar constrs.	Pierre-Marie Pédrot	2017-02-14
\| \| \| \| \| \| \| \| \| \| \| \|	Incidentally, this fixes a printing bug in output/inference.v where the displayed name of an evar was the wrong one because its type was not evar-expanded enough.
* \|	Making Evd independent from Namegen.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Moving printing code from Evd to Termops.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Chasing a few unsafe constr coercions.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Do not ask for a normalized goal to get hypotheses and conclusions.	Pierre-Marie Pédrot	2017-02-14
\| \| \| \| \| \| \| \| \| \|	This is now useless as this returns evar-constrs, so that all functions acting on them should be insensitive to evar-normalization.
* \|	Definining EConstr-based contexts.	Pierre-Marie Pédrot	2017-02-14
\| \| \| \| \| \| \| \| \| \| \| \|	This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr.
* \|	Evar-normalizing functions now act on EConstrs.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Ltac now uses evar-based constrs.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Removing some return type compatibility layers in Termops.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Reductionops now return EConstrs.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Proofview.Goal primitive now return EConstrs.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Eliminating parts of the right-hand side compatibility layer	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Rewrite API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Hints API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Leminv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Inv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Contradiction API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Equality API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Tactics API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Hipattern API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Tacticals API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Clenv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Refine API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Making judgment type generic over the type of inner constrs.	Pierre-Marie Pédrot	2017-02-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This allows to factorize code and prevents the unnecessary use of back and forth conversions between the various types of terms. Note that functions from typing may now raise errors as PretypeError rather than TypeError, because they call the proper wrapper. I think that they were wrongly calling the kernel because of an overlook of open modules.
* \|	Unification API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Pretyping API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Cases API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Typeclasses API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Tacred API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Evarconv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Evarsolve API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Reductionops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Termops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
\| *	Proofview: tclINDEPENDENTL	Enrico Tassi	2017-02-10
\| \|
\| *	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-02-01
\| \|\