coq - The formal proof system

Age	Commit message (Collapse)	Author
2018-09-27	Possible abstractions over goal variables when inferring match return clause.	Hugo Herbelin
	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.
2018-09-27	Trying an abstracting dependencies heuristic for the match return clause ↵	Hugo Herbelin
	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.
2018-09-27	Trying a no-inversion no-dependency heuristic for match return clause.	Hugo Herbelin
	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.
2016-10-11	Reverting generalization and cleaning of the return clause inference in v8.6.	Hugo Herbelin
	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.
2016-09-26	Posssible abstractions over goal variables when inferring match return clause.	Hugo Herbelin
	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.
2016-09-26	Trying an abstracting dependencies heuristic for the match return clause ↵	Hugo Herbelin
	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.
2016-09-26	Trying a no-inversion no-dependency heuristic for match return clause.	Hugo Herbelin
	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.
2016-08-20	Fixing an anomaly in printing a unification error message.	Hugo Herbelin

2006-09-23	Correction d'un bug de coercion de pattern introduit dans la 8.1beta	herbelin
	(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
2006-01-30	Prise en compte coercions autour des sous-termes filtrés (si non dépendants)	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7961 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-21	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19	Un peu plus d'inférence des ? traitée par le Cases	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2323 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-11	Test des coercions dans les motifs	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2284 85f007b7-540e-0410-9357-904b9bb8a0f7