coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Reverting generalization and cleaning of the return clause inference in v8.6.	Hugo Herbelin	2016-10-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The move to systematically trying small inversion first bumps sometimes as feared to the weakness of unification (see #5107). ---- Revert "Posssible abstractions over goal variables when inferring match return clause." This reverts commit 0658ba7b908dad946200f872f44260d0e4893a94. Revert "Trying an abstracting dependencies heuristic for the match return clause even when no type constraint is given." This reverts commit 292f365185b7acdee79f3ff7b158551c2764c548. Revert "Trying a no-inversion no-dependency heuristic for match return clause." This reverts commit 2422aeb2b59229891508f35890653a9737988c00.
*	Posssible abstractions over goal variables when inferring match return clause.	Hugo Herbelin	2016-09-26
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	The no-inversion and maximal abstraction over dependencies now supports abstraction over goal variables rather than only on "rel" variables. In particular, it now works consistently using "intro H; refine (match H with ... end)" or "refine (fun H => match H with ... end)". By doing so, we ensure that all three strategies are tried in all situations where a return clause has to be inferred, even in the context of a "refine". See antepenultimate commit for discussion.
*	Trying an abstracting dependencies heuristic for the match return clause ↵	Hugo Herbelin	2016-09-26
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	even when no type constraint is given. This no-inversion and maximal abstraction over dependencies in (rel) variables heuristic was used only when a type constraint was given. By doing so, we ensure that all three strategies "inversion with dependencies as evars", "no-inversion and maximal abstraction over dependencies in (rel) variables", "no-inversion and no abstraction over dependencies" are tried in all situations where a return clause has to be inferred. See penultimate commit for discussion.
*	Trying a no-inversion no-dependency heuristic for match return clause.	Hugo Herbelin	2016-09-26
\| \| \| \| \| \| \| \|	The no-inversion no-dependency heuristic was used only in the absence of type constraint. We may now use it also in the presence of a type constraint. See previous commit for discussion.
*	Fixing an anomaly in printing a unification error message.	Hugo Herbelin	2016-08-20
\|
*	Correction d'un bug de coercion de pattern introduit dans la 8.1beta	herbelin	2006-09-23
\| \| \| \| \| \| \| \|	(les coercions ne marchaient plus quand le type du terme à filtrer était connu). Ajout d'un test pour ce bug et pour le bug #1168. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9169 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte coercions autour des sous-termes filtrés (si non dépendants)	herbelin	2006-01-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7961 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin	2005-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Un peu plus d'inférence des ? traitée par le Cases	herbelin	2001-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2323 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Test des coercions dans les motifs	herbelin	2001-12-11
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2284 85f007b7-540e-0410-9357-904b9bb8a0f7