coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Removing compatibility layers from Tacticals	Pierre-Marie Pédrot	2017-02-14
\|
*	Cleaning up interfaces.	Pierre-Marie Pédrot	2017-02-14
\| \| \| \| \|	We make mli files look to what they were looking before the move to EConstr by opening this module.
*	Omega API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Micromega API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot	2017-02-14
\|
*	Funind API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Removing compatibility layers related to printing.	Pierre-Marie Pédrot	2017-02-14
\|
*	Ltac now uses evar-based constrs.	Pierre-Marie Pédrot	2017-02-14
\|
*	Removing compatibility layers in Retyping	Pierre-Marie Pédrot	2017-02-14
\|
*	Removing some return type compatibility layers in Termops.	Pierre-Marie Pédrot	2017-02-14
\|
*	Setoid_ring API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Cc API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Quote API using EConstr.	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
\|
*	Tauto API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Rewrite API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	G_class API using Econstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	G_auto API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Extratactics API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Tactic_matching API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Eqdecide API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Class_tactics API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Eauto API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Auto 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
\|
*	Elim 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
\|
*	Tacmach API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Refine API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Goal API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Cleaning up opening of the EConstr module in pretyping folder.	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
\|
*	Coercion API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Classops 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
\|
*	Constr_matching API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Patternops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|