aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Lists/List.v
Commit message (Collapse)AuthorAge
* Very-small-step policy changes to the library.Gravatar herbelin2009-06-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12166 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add lemmas on lists: nth_default_eq, map_nth_errorGravatar glondu2008-08-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11310 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cyclic31: migrate auxiliary lemmas to their legitimate filesGravatar letouzey2008-05-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10999 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ]Gravatar herbelin2008-05-09
| | | | | | | pour les listes (trop contraignant) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10913 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout notation [ x ; ... ; y ] dans list_scope. Changement de laGravatar herbelin2008-04-29
| | | | | | | | | | | syntaxe interne de ring_lookup et field_lookup qui n'était pas assez robuste pour supporter une syntaxe [ ... ] dans constr. Déplacement de now_show de List.v vers Tactics.v, déplacement de "[ _ ]" au niveau 0. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10872 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack on using metas eagerly in auto, only done in "new auto" forGravatar msozeau2008-04-28
| | | | | | | | now. Fix proof scripts that failed correspondingly. Should make many contribs compile again... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10863 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fix bug in unification not taking into account the right metaGravatar msozeau2008-04-27
| | | | | | | | | | | | | substitution. Makes unification succeed a bit more often, hence auto works better in some cases. - Backtrack the changes of auto using Hint Unfold to do more delta and add a new tactic "new auto" which does that, for compatibility. The first fix may have a big impact on the contribs, whereas the second should make them compile again... we'll see. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10855 85f007b7-540e-0410-9357-904b9bb8a0f7
* - A little cleanup in Classes/*. Separate standard morphisms onGravatar msozeau2008-04-08
| | | | | | | | | | | | | | | | | relf/sym/trans relations from morphisms on prop connectives and relations. - Add general order theory on predicates, instantiated for relations. Derives equivalence, implication, conjunction and disjunction as liftings from propositional connectives. Can be used for n-ary homogeneous predicates thanks to a bit of metaprogramming with lists of types. - Rebind Setoid_Theory to use the Equivalence record type instead of declaring an isomorphic one. One needs to do "red" after constructor to get the same statements when building objects of type Setoid_Theory, so scripts break. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10765 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1819Gravatar notin2008-04-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10734 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merged revisions ↵Gravatar msozeau2007-12-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,10398,10403-10408 via svnmerge from svn+ssh://msozeau@scm.gforge.inria.fr/svn/coq/branches/TypeClasses ........ r10358 | msozeau | 2007-12-10 15:42:53 +0100 (Mon, 10 Dec 2007) | 1 line Comment grammar error ........ r10359 | msozeau | 2007-12-10 16:04:09 +0100 (Mon, 10 Dec 2007) | 7 lines The initial Type Classes patch. This patch introduces type classes and instance definitions a la Haskell. Technically, it uses the implicit arguments mechanism which was extended a bit. The patch also introduces a notation for explicitely marking implicit, maximally inserted parameters. It includes the tactic redefinition code too (Ltac tac ::= foo redefines tac). ........ r10360 | msozeau | 2007-12-10 16:14:30 +0100 (Mon, 10 Dec 2007) | 1 line Fix interface ........ r10361 | msozeau | 2007-12-10 16:28:19 +0100 (Mon, 10 Dec 2007) | 1 line Fix more xlate code ........ r10362 | msozeau | 2007-12-11 02:00:53 +0100 (Tue, 11 Dec 2007) | 3 lines Update coqdoc for type classes, fix proof state not being displayed on Next Obligation. ........ r10365 | msozeau | 2007-12-11 14:22:35 +0100 (Tue, 11 Dec 2007) | 3 lines Bug fixes in Instance decls. ........ r10371 | msozeau | 2007-12-12 21:17:30 +0100 (Wed, 12 Dec 2007) | 3 lines Streamline typeclass context implementation, prepare for class binders in proof statements. ........ r10372 | msozeau | 2007-12-12 22:03:38 +0100 (Wed, 12 Dec 2007) | 1 line Minor cosmetic fixes: allow sorts as typeclass param instances without parens and infer more types in class definitions ........ r10373 | msozeau | 2007-12-13 00:35:09 +0100 (Thu, 13 Dec 2007) | 2 lines Better names in g_vernac, binders in Lemmas and Context [] to introduce a typeclass context. ........ r10377 | msozeau | 2007-12-13 18:34:33 +0100 (Thu, 13 Dec 2007) | 1 line Stupid bug ........ r10383 | msozeau | 2007-12-16 00:04:48 +0100 (Sun, 16 Dec 2007) | 1 line Bug fixes in name handling and implicits, new syntax for using implicit mode in typeclass constraints ........ r10384 | msozeau | 2007-12-16 15:53:24 +0100 (Sun, 16 Dec 2007) | 1 line Streamlined implementation of instances again, the produced typeclass is a typeclass constraint. Added corresponding implicit/explicit behaviors ........ r10394 | msozeau | 2007-12-18 23:42:56 +0100 (Tue, 18 Dec 2007) | 4 lines Various fixes for implicit arguments, new "Enriching" kw to just enrich existing sets of impl args. New syntax !a to force an argument, even if not dependent. New tactic clrewrite using a setoid typeclass implementation to do setoid_rewrite under compatible morphisms... very experimental. Other bugs related to naming in typeclasses fixed. ........ r10395 | msozeau | 2007-12-19 17:11:55 +0100 (Wed, 19 Dec 2007) | 3 lines Progress on setoids using type classes, recognize setoid equalities in hyps better. Streamline implementation to return more information when resolving setoids (return the results setoid). ........ r10398 | msozeau | 2007-12-20 10:18:19 +0100 (Thu, 20 Dec 2007) | 1 line Syntax change, more like Coq ........ r10403 | msozeau | 2007-12-21 22:30:35 +0100 (Fri, 21 Dec 2007) | 1 line Add right-to-left rewriting in class_setoid, fix some discharge/substitution bug, adapt test-suite to latest syntax ........ r10404 | msozeau | 2007-12-24 21:47:58 +0100 (Mon, 24 Dec 2007) | 2 lines Work on type classes based rewrite tactic. ........ r10405 | msozeau | 2007-12-27 18:51:32 +0100 (Thu, 27 Dec 2007) | 2 lines Better evar handling in pretyping, reorder theories/Program and add some tactics for dealing with subsets. ........ r10406 | msozeau | 2007-12-27 18:52:05 +0100 (Thu, 27 Dec 2007) | 1 line Forgot to add a file ........ r10407 | msozeau | 2007-12-29 17:19:54 +0100 (Sat, 29 Dec 2007) | 4 lines Generalize usage of implicit arguments in terms, up to rawconstr. Binders are decorated with binding info, either Implicit or Explicit for rawconstr. Factorizes code for typeclasses, topconstrs decorations are Default (impl|expl) or TypeClass (impl|expl) and implicit quantification is resolve at internalization time, getting rid of the arbitrary prenex restriction on contexts. ........ r10408 | msozeau | 2007-12-31 00:58:50 +0100 (Mon, 31 Dec 2007) | 4 lines Fix parsing of subset binders, bugs in subtac_cases and handling of mutual defs obligations. Add useful tactics to Program.Subsets. ........ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10410 85f007b7-540e-0410-9357-904b9bb8a0f7
* small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is Gravatar letouzey2007-11-06
| | | | | | | | more general. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10295 85f007b7-540e-0410-9357-904b9bb8a0f7
* two additionnal results on list append (coming from ↵Gravatar letouzey2007-11-01
| | | | | | theories/ints/List/ListAux.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10284 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement des propriétés générales de BinList dans List et des ↵Gravatar herbelin2006-10-26
| | | | | | | | | tactiques de BinList dans un nouveau ListTactics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9290 85f007b7-540e-0410-9357-904b9bb8a0f7
* Indentation + typoGravatar notin2006-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9104 85f007b7-540e-0410-9357-904b9bb8a0f7
* Argument Scope de list déplacé dans List.vGravatar herbelin2006-07-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9035 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quelques Hint inutilesGravatar herbelin2006-07-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9025 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Déplacement des types paramétriques prod, sum, option, identity,Gravatar herbelin2006-05-28
| | | | | | | | | | | sig, sig2, sumor, list et vector dans Type - Branchement de prodT/listT vers les nouveaux prod/list - Abandon sigS/sigS2 au profit de sigT et du nouveau sigT2 - Changements en conséquence dans les théories (notamment Field_Tactic), ainsi que dans les modules ML Coqlib/Equality/Hipattern/Field git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8866 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo dans List.vGravatar notin2006-05-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8826 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de [count_occ] dans List.vGravatar notin2006-05-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8824 85f007b7-540e-0410-9357-904b9bb8a0f7
* etoffage des notions de permutations (a la fois List.Permutation et ↵Gravatar letouzey2006-05-16
| | | | | | Permutation.permutation) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8823 85f007b7-540e-0410-9357-904b9bb8a0f7
* In_dec de nouveau transparentGravatar letouzey2006-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8816 85f007b7-540e-0410-9357-904b9bb8a0f7
* r9089@thot: notin | 2006-05-10 14:40:51 +0200Gravatar notin2006-05-11
| | | | | | | Réorganisation List.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8803 85f007b7-540e-0410-9357-904b9bb8a0f7
* versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmesGravatar letouzey2006-04-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8686 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification des propriétés (svn:executable)Gravatar notin2006-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8642 85f007b7-540e-0410-9357-904b9bb8a0f7
* In_dec transparent (wish #902)Gravatar herbelin2004-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6483 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle en-têteGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout delimiteur et arguments de scope pour listGravatar herbelin2003-12-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5145 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ↵Gravatar herbelin2003-11-29
| | | | | | par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage en v8 de PolyList en List et List en MonoListGravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4557 85f007b7-540e-0410-9357-904b9bb8a0f7
* option -dump-glob pour coqdocGravatar filliatr2002-02-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
* Library doc adjustments (until page 140)Gravatar coq2001-04-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1655 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise de (*i autour CVS infoGravatar mohring2001-04-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1620 85f007b7-540e-0410-9357-904b9bb8a0f7
* entetesGravatar filliatr2001-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout du Let pour le langage de tactiquesGravatar delahaye2000-12-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1231 85f007b7-540e-0410-9357-904b9bb8a0f7
* theories/ListsGravatar filliatr2000-06-21
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@508 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-12 19:55:07 +0000