coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	instanciation is French, instantiation is English	Jason Gross	2014-08-25
\|
*	Unification in Evar_conv uses an abstract machine state	pboutill	2012-08-09
\| \| \| \| \| \| \| \| \|	It uses a term in front of a stack instead of a term in front of a list of applied terms. From outside of eq_appr_x nothing should have changed. Nasty evar instantiation bug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15719 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Completing r14538 (Chung-Kil Hur's trick for fast dependently-typed	herbelin	2011-10-11
\| \| \| \| \| \| \| \| \| \| \|	second-order matching) which was not working correctly in the general case. Also made that second-order matching for tactics (abstract_list_all) uses this algorithm, along the lines of a proposal first experimented by Dan Grayson (see unification.v). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14549 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added full pattern-unification on Meta for tactic unification.	herbelin	2011-06-13
\| \| \| \| \| \| \|	No way to control it yet; maybe flag use_evars_pattern_unification should be generalized for that purpose. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14199 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added a new flag for freezing evars in tactic unification. Used this	herbelin	2011-06-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	flag to forbid rewriting tactics to instantiate an evar of the goal while looking for subterms (this is not clear that we always want that for rewrite but we certainly want it for autorewrite; see comments by Charguéraud on coqdev Oct 2010). In a few cases in the theories, a pre-existing evar of an hyp used for rewriting is instantiated by the rewriting step. Let's accept this at the current time. We have to make progress towards documenting and stabilizing the strategy for matching/unifying subterms in rewrite/induction/set... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14190 85f007b7-540e-0410-9357-904b9bb8a0f7
*	test-suite: fix success/unification.v	glondu	2010-10-07
\| \| \| \| \| \|	This test it not relevant anyway, thanks to eta... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13513 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Commit 12906 continued (forgotten file).	herbelin	2010-04-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12907 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adding a regression test about Bauer's example on coq-club of	herbelin	2009-06-02
\| \| \| \| \| \| \|	rewriting using eta. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12161 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Retrait d'un test commité par erreur en 10947	herbelin	2008-05-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10949 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Intégration de micromega ("omicron" pour fourier et sa variante sur Z,	herbelin	2008-05-19
\| \| \| \| \| \| \| \| \| \| \|	"micromega" et "sos" pour les problèmes non linéaires sous-traités à csdp); mise en place d'un cache pour pouvoir rejouer les preuves sans avoir besoin de csdp (pour l'instant c'est du bricolage, faudra affiner cela). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10947 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Résolution des problèmes ambigus d'inférence du type de retour des	herbelin	2008-05-14
\| \| \| \| \| \| \| \| \|	problèmes de filtrage au nivau de consider_remaining_unif_problems (résoud en particulier le "bug" #1851). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10927 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Un peu de doc, préparation du CHANGES pour la release.	herbelin	2008-04-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Re-restriction de inversion (après la correction des bugs - et notamment du "Unknown meta" qui apparaissait parfois -, inversion devenait capable d'agir sur des buts non atomiques, ce qui crée quelques incompatibilités, typiquement dans CoRN où inversion est utilisé dans un rôle de discriminate; en attendant de voir, on revient à la sémantique initiale). - Généralisation de Local/Global dans Implicit Arguments pour avoir un fonctionnement plus uniforme et plus facile à documenter. - Code mort (clenv.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10796 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Backtrack sur le test censé discriminer entre une erreur d'evar non	herbelin	2008-03-15
\| \| \| \| \| \| \| \| \| \|	résolue et une anomalie. Il ne marche pas. La question de trouver la bonne manière de tester qu'un exemple renvoie une erreur (non rattrapable par tactique) et une anomalie reste ouverte. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10675 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)	herbelin	2008-03-10
\| \| \| \| \| \| \| \| \|	- Correction bug des filtres dans define_evar_as_abstraction - Nettoyage, documentation et réorganisations diverses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10650 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un bug "ancestral": apply ne savait pas unifier ?n=?n	herbelin	2008-03-06
\| \| \| \| \| \| \| \| \|	dans certains cas. Branchement au passage de w_unify vers evar_conv et solve_simple_eqn en cas d'équations entre Evars. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10623 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'une typo restant du commit 10557 et cause d'échec de contribs	herbelin	2008-03-05
\| \| \| \| \| \| \| \|	telles que Godel git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10622 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Redondance erronée dans les tests	herbelin	2007-01-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9533 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
*	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
*	Diverses modifications autour de l'unification modulo conversion:	herbelin	2006-08-28
	- extension de l'unification au cas de motifs (au sens de Dale Miller) [appel de solve_pattern_eqn dans evar_conv_x], - correction de bugs présumés dans real_clean et do_restrict_hyp (prise en compte de la taille courante du contexte de de Bruijn), - ajout d'une heuristique de beta-reduction de tete dans real_clean (cf test-suite/success/unification.v), - suppression de certains "try ... with _ => ...". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9088 85f007b7-540e-0410-9357-904b9bb8a0f7