aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/unification.v
AgeCommit message (Collapse)Author
2017-10-19Moving bug numbers to BZ# format in the test-suite.Théo Zimmermann
Compared to the original proposition (59a594b in #960), this commit only changes files containing bug numbers that are also PR numbers.
2017-05-05Adding a test-suite pattern-unification example that Econstr fixed.Hugo Herbelin
2014-08-25instanciation is French, instantiation is EnglishJason Gross
2012-08-09Unification in Evar_conv uses an abstract machine statepboutill
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
2011-10-11Completing r14538 (Chung-Kil Hur's trick for fast dependently-typedherbelin
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
2011-06-13Added full pattern-unification on Meta for tactic unification.herbelin
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
2011-06-12Added a new flag for freezing evars in tactic unification. Used thisherbelin
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
2010-10-07test-suite: fix success/unification.vglondu
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
2010-04-07Commit 12906 continued (forgotten file).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12907 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-02Adding a regression test about Bauer's example on coq-club ofherbelin
rewriting using eta. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12161 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-20Retrait d'un test commité par erreur en 10947herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10949 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-19Intégration de micromega ("omicron" pour fourier et sa variante sur Z,herbelin
"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
2008-05-14Résolution des problèmes ambigus d'inférence du type de retour desherbelin
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
2008-04-15- Un peu de doc, préparation du CHANGES pour la release.herbelin
- 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
2008-03-15Backtrack sur le test censé discriminer entre une erreur d'evar nonherbelin
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
2008-03-10Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)herbelin
- 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
2008-03-06Correction d'un bug "ancestral": apply ne savait pas unifier ?n=?nherbelin
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
2008-03-05Correction d'une typo restant du commit 10557 et cause d'échec de contribsherbelin
telles que Godel git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10622 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-25Redondance erronée dans les testsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9533 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-22Correction d'un bug d'unification-pattern dans l'algo d'unificationherbelin
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
2006-11-19Raffinement de l'unification de "apply": mémorisation de certainsherbelin
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
2006-09-12Ajout unification pattern dans l'algorithme d'unification desherbelin
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
2006-08-28Diverses modifications autour de l'unification modulo conversion:herbelin
- 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 18:35:09 +0000