aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/Record.v
AgeCommit message (Collapse)Author
2020-10-16Fixes/enhancements with local definitions in records.Hugo Herbelin
Fixes implicit arguments from the body of a defined field not taken into account. Get (a bit) more information for detection of SProp relevance in implicitly-typed defined field. (It should be done at the very end of the inference phase, though, because some evars may not yet be instantiated.)
2020-04-30do not re-export ListNotations from Program: fix testsuiteAntonio Nikishaev
2018-03-30Change Implicit Arguments to Arguments in test-suiteJasper Hugunin
2017-05-31More precise on preventing clash between bound vars name and hidden impargs.Hugo Herbelin
We want to avoid capture in "Inductive I {A} := C : forall A, I". But in "Record I {A} := { C : forall A, A }.", non recursivity ensures that no clash will occur. This fixes previous commit, with which it could possibly be merged.
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-07-15- Granted wish #2138 (support for local binders in syntax of Record fields).herbelin
- Add tests related to commits 12229 (bug #2117) and 12241 (bug #2139). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12242 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-22Fixes in the documentation of [dependent induction] and test-suitemsozeau
scripts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11839 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-07Add some example uses of the new record features in Record.v:msozeau
- introduction notation with missing fields and interaction with Program. - Ability to add (currently a single) "where notation" clause to each field. - Use every information available to do type inference and internalisation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11552 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-21Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-15Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à ↵herbelin
une sorte git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3497 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:53:34 +0000