coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Utilisation de l'environnement pour l'affichage de certains messages d'erreurs	herbelin	2007-02-21
\| \| \| \| \| \| \|	+ petit nettoyage himsg.ml + petite uniformisation erreurs CannotUnify git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9668 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un bug d'unification-pattern dans l'algo d'unification	herbelin	2007-01-22
\| \| \| \| \| \| \| \|	des tactiques (ne marchait que si l'instance était une application). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9516 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Raffinement de l'unification de "apply": mémorisation de certains	herbelin	2006-11-19
\| \| \| \| \| \| \| \| \|	degrés de liberté concernant les instances de méta (cumulativité et possibilité d'éta-expansion) de telle sorte que la fusion d'équations se fasse modulo ces degrés de liberté. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9389 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un bug dans l'unification: lors de l'unification d'un meta m et ↵	notin	2006-10-05
\| \| \| \| \| \|	d'un constr c, on vérifie que c est clos dans l'environnement de m (#1183) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9217 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Abandon unification pattern des evars dans apply: combiné avec le	herbelin	2006-09-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	backtrack de eauto et le partage des evars entre buts, cela fait davantage de choix irréversibles avec rupture de compatibilité. Exemple: but 1: \|- P ?f but 2: H1:a=b, H2:c=c, H3:g a = g b \|- ?f a = ?f b eauto sur le but 2 peut trouver au moins 3 solutions: 1- avec unif premier ordre, il peut trouver ?f=g, en appliquant exact H3 2- avec unif pattern, il peut trouver ?f=\_.c, en appliquant exact H2 3- en s'y prenant bien, il devrait pouvoir laisser ?f ouvert en appliquant f_equal H1 Dans certains exemples (Orsay/FSets/PrecedenceGraph/PrecedenceGraph.v en l'occurrence), ajouter l'unif pattern fait adopter la solution 2 plutôt que la solution 3. En attente d'un meilleur algorithme, abandon donc de l'unif pattern des evars pour apply (ce qui n'empêche pas que, déjà, la situation actuelle, qui utilise l'unif premier ordre, peut conduire à faire des mauvais choix -- mais au moins on reste compatible...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9134 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction conflit Meta/Evar dans commit précédent et extension au	herbelin	2006-09-12
\| \| \| \| \| \| \|	passage de l'unification pattern au cas tant des Meta que des Evar. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9132 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout unification pattern dans l'algorithme d'unification des	herbelin	2006-09-12
\| \| \| \| \| \| \|	tactiques (unification.ml) + renommages (evarconv.ml) + exemple (unification.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9131 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Standardisation du nom des méthodes de Evd	herbelin	2006-04-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8759 85f007b7-540e-0410-9357-904b9bb8a0f7
*	eradication de Evarutil.w_Define	barras	2005-06-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7113 85f007b7-540e-0410-9357-904b9bb8a0f7
*	WARNING: unification changed (to fix a bug).	sacerdot	2005-05-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	1. When matching ?i[sigma] against t' in some cases ?i was instantiated with t' ignoring the explicit substitution sigma (i.e. always doing mimick); however, when t' occurs in sigma ?i can be instatiated with a Var/Rel (i.e. doing projection). The new behaviour is not equivalent to the old one (even up to bugs) since the new behaviour may accept not well typed instantiations and fail only later whereas the old (but buggy) behaviour failed immediately. 2. Second bug fixed: it was the case that instantiating and evar doing projection did not check whether the body of the evar contained metavariables (that breaks a Coq invariant). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7067 85f007b7-540e-0410-9357-904b9bb8a0f7
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
*	?(mod_delta=true) parameter added to each unification function.	sacerdot	2004-09-27
\| \| \| \| \| \| \| \|	mod_delta = true if the unification is done modulus delta conversion (of closed terms). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6142 85f007b7-540e-0410-9357-904b9bb8a0f7
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6113 85f007b7-540e-0410-9357-904b9bb8a0f7
*	hiding the meta_map in evar_defs	barras	2004-09-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6109 85f007b7-540e-0410-9357-904b9bb8a0f7
*	inclusion de meta_map dans evar_defs	barras	2004-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6099 85f007b7-540e-0410-9357-904b9bb8a0f7
*	unification encore...	barras	2004-09-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6085 85f007b7-540e-0410-9357-904b9bb8a0f7
*	deuxieme vague de modifs: evar_defs fonctionnel	barras	2004-09-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6071 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mimick: unify types before making assignation	barras	2004-09-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6067 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bad env in mimick code	barras	2004-09-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6065 85f007b7-540e-0410-9357-904b9bb8a0f7
*	deplacement de clenv vers pretyping	barras	2004-09-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6058 85f007b7-540e-0410-9357-904b9bb8a0f7
*	premiere reorganisation de l\'unification	barras	2004-09-03
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7