aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/CanonicalStructure.v
AgeCommit message (Collapse)Author
2021-04-22Enable canonical `fun _ => _` projections.Jan-Oliver Kaiser
2019-12-24[Attributes] accept #[canonical] (Let|Definition)Enrico Tassi
2019-12-24[CS] Allow a variable introduced with Let to be a canonical instanceEnrico Tassi
2019-12-02[CS] support #[local] attributeEnrico Tassi
2008-06-29Préférence donnée aux constantes qui ne sont pas des projectionsherbelin
canoniques lors d'une unification constante/constante s'apprêtant à déplier l'une des deux constantes (suggestion des utilisateurs de structures canoniques), ceci afin de préserver des possibilités ultérieures de résolution d'evars par équipement en structure canonique. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11187 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-23Wish #1187 granted (support for canonical structures that are recordsherbelin
only up to some preliminary reductions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9166 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-07Correction bug 1172 + correction en passant de la taille des paramètres de ↵herbelin
famille git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9033 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-12 03:02:07 +0000