coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fixing an extra bug with pattern_of_constr.	Hugo Herbelin	2017-05-19
\| \| \| \| \| \| \| \|	Ensure in type constr_pattern that those preexisting existential variables of the goal which do not contribute as pattern variables are expanded: constr_pattern is not observed up to evar expansion (like EConstr does), so we need to pre-normalize defined evars in patterns to that matching against an EConstr works.
*	Fixing side bug in db37c9f3f32ae7 delaying interpretation of the	Hugo Herbelin	2014-11-16
\| \| \| \| \|	right-hand side of a "change with": the rhs lives in the toplevel environment.
*	Relaxing again the test on types of replacements in tactic change	Hugo Herbelin	2014-10-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	(continuation of 3087e0012eb12833a79b and 1f05decaea97f1dc). It may be the case that the new expression lives in a higher sorts and the context where it is substituted in supports it. So, it is too strong to expect that, when the substituted objects are types, the sort of the new one is smaller than the sort of the original one. Consider e.g. Goal @eq Type nat nat. change nat with (@id Type nat). which is a correct replacement, even if (id Type nat) is in a higher sort. Introducing typing in "contextually" would be a big change for a little numbers of uses, so we instead (hackily) recheck the whole term (even though typing with evars uses evar_conv which accept to unify Type with Set, leading to wrongly accept "Goal @eq Set nat nat. change nat with (@id Type nat).". Evar conv is however rejecting Prop=Type.)
*	Fixing #3641 (loop in e_contextually, introduced in r16525).	Hugo Herbelin	2014-09-19
\|
*	Kills the useless tactic annotations "in \|- *"	letouzey	2012-07-05
\| \| \| \| \| \| \|	Most of these heavyweight annotations were introduced a long time ago by the automatic 7.x -> 8.0 translator git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
*	It happens that the type inference algorithm (pretyping) did not check	herbelin	2011-10-05
\| \| \| \| \| \| \| \| \| \|	that the return predicate of the match construction is at an allowed sort, resulting in tactics possibly manipulating ill-typed terms. This is now fixed, Incidentally removed in pretyping an ill-placed coercion. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14508 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing bug #2146 (broken selection of occurrences in "change").	herbelin	2009-12-30
\| \| \| \| \| \| \| \| \| \|	In trunk the different possible combinations of "at" and "in" with occurrences are taken into account. In 8.2 branch, it remains fragile (syntaxes that were accepted remain accepted and a message warns if the occurrences coming after the "with" are not taken into account). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12614 85f007b7-540e-0410-9357-904b9bb8a0f7
*	In "simpl c" and "change c with d", c can be a pattern.	herbelin	2009-12-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12608 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un bug à l'interprétation de "change" (on exigeait que	herbelin	2008-02-06
	l'argument soit un type même lorsque c'était un terme qu'on convertissait). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10518 85f007b7-540e-0410-9357-904b9bb8a0f7