aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Lists
Commit message (Collapse)AuthorAge
* Improving abbreviations/notations + backtrack of semantic change in r12439Gravatar herbelin2009-11-11
| | | | | | | | | | | | | | | | | | | | | | | | | | - Deactivation of short names registration and printing for abbreviations to identical names, what avoids printing uselessly qualified names binding where the short name is in fact equivalent. - New treatment of abbreviations to names: don't insert any maximally inserted implicit arguments at all at the time of the abbreviation and use the regular internalization strategy to have them inserted at use time. - The previous modifications altogether make redirections of qualified names easier and avoid the semantic change of r12349 and hence allows to keep "Notation b := @a" as it was before, i.e. as a notation for the deactivation of the implicit arguments of a. - Took benefit of these changes and updated nil/cons/list/app redefinition in "List.v". - Fixed parsing/printing notation bugs (loop on partially applied abreviations for constructors in constrintern.ml + bad reverting of notations with holes that captured non anonymous variables in match_cases_pattern). - Add support for parsing/printing abbreviations to @-like constructors and for reverting printing for abbreviations to constructors applied to parameters only (function extern_symbol_pattern). - Minor error messages fixes and minor APIs cleaning. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12494 85f007b7-540e-0410-9357-904b9bb8a0f7
* List + SetoidList : some cleanup around predicates Exists, Forall, Forall2, ↵Gravatar letouzey2009-11-02
| | | | | | ForallPairs, etc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12459 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove various useless {struct} annotationsGravatar letouzey2009-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12458 85f007b7-540e-0410-9357-904b9bb8a0f7
* list, length, app are migrated from List to DatatypesGravatar letouzey2009-11-02
| | | | | | | | | | | | | | | | | This allows easier handling of dependencies, for instance RelationClasses won't have to requires List (which itself requires part of Arith, etc). One of the underlying ideas is to provide setoid rewriting in Init someday. Thanks to some notations in List, this change should be fairly transparent to the user. For instance, one could see that List.length is a notation for (Datatypes.)length only when doing a Print List.length. For these notations not to be too intrusive, they are hidden behind an explicit Export of Datatypes at the end of List. This isn't very pretty, but quite handy. Notation.ml is patched to stop complaining in the case of reloading the same Delimit Scope twice. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12452 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix flat_map definition so that it plays nicely with fixGravatar glondu2009-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12444 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge SetoidList2 into SetoidList.Gravatar letouzey2009-10-19
| | | | | | | | | This file contains low-level stuff for FSets/FMaps. Switching it to the new version (the one using Equivalence and so on instead of eq_refl/eq_sym/eq_trans and so on) only leads to a few changes in FSets/FMaps that are minor and probably invisible to standard users. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12400 85f007b7-540e-0410-9357-904b9bb8a0f7
* MSets: a new generation of FSetsGravatar letouzey2009-10-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Same global ideas (in particular the use of modules/functors), but: - frequent use of Type Classes inside interfaces/implementation. For instance, no more eq_refl/eq_sym/eq_trans, but Equivalence. A class StrictOrder for lt in OrderedType. Extensive use of Proper and rewrite. - now that rewrite is mature, we write specifications of set operators via iff instead of many separate requirements based on ->. For instance add_spec : In y (add x s) <-> E.eq y x \/ In x s. Old-style specs are available in the functor Facts. - compare is now a pure function (t -> t -> comparison) instead of returning a dependent type Compare. - The "Raw" functors (the ones dealing with e.g. list with no sortedness proofs yet, but morally sorted when operating on them) are given proper interfaces and a generic functor allows to obtain a regular set implementation out of a "raw" one. The last two points allow to manipulate set objects that are completely free of proof-parts if one wants to. Later proofs will rely on type-classes instance search mechanism. No need to emphasis the fact that this new version is severely incompatible with the earlier one. I've no precise ideas yet on how allowing an easy transition (functors ?). For the moment, these new Sets are placed alongside the old ones, in directory MSets (M for Modular, to constrast with forthcoming CSets, see below). A few files exist currently in version foo.v and foo2.v, I'll try to merge them without breaking things. Old FSets will probably move to a contrib later. Still to be done: - adapt FMap in the same way - integrate misc stuff like multisets or the map function - CSets, i.e. Sets based on Type Classes : Integration of code contributed by S. Lescuyer is on the way. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12384 85f007b7-540e-0410-9357-904b9bb8a0f7
* Implicit argument of Logic.eq become maximally insertedGravatar letouzey2009-10-08
| | | | | | | | | This allow in particular to write eq instead of (@eq _) in signatures of morphisms. I dont really see how this could break existing code, no change in the stdlib was mandatory. We'll check the contribs tomorrow... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12379 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove useless MonoList.vGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12339 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* adds a property on mapGravatar bertot2009-08-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12285 85f007b7-540e-0410-9357-904b9bb8a0f7
* adds lemmas on interactions between existsb, forallb, and appGravatar bertot2009-08-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12284 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Add more precise error localisation when one of the application failsGravatar herbelin2009-08-04
| | | | | | | | | | | | in a chain of apply or apply-in. - Improved comments on the notions of permutation used in the library (still the equality relation in file Permutation.v misses the property of being effectively an equivalence relation, hence missing expected properties of this notion of permutation). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12261 85f007b7-540e-0410-9357-904b9bb8a0f7
* List: add a iff-based lemma about In and ++Gravatar letouzey2009-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12249 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo in a commentGravatar letouzey2009-07-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12243 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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
* fixed ring/field warning about hyp cleaning upGravatar barras2009-03-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11993 85f007b7-540e-0410-9357-904b9bb8a0f7
* - gros commit sur ring et field: passage des arguments simplifieGravatar barras2009-03-17
| | | | | | | | | | | - tacinterp.ml: les arguments tactiques de Tactic Notation n'etaient pas evalues, laissant des variables libres (symptome: exc Not_found) - reals: Open Local --> Local Open - ListTactics: syntaxe des listes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11989 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various little fixes:Gravatar msozeau2009-01-18
| | | | | | | | | | | | - allow a new line after a (** printing *) directive in coqdoc so as not to output spurious new lines. - never directly unify the lemma with an evar in setoid_rewrite (they act as opaque constants). - Fix a useless dependency introduced by tauto which splits a record in SetoidList. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11799 85f007b7-540e-0410-9357-904b9bb8a0f7
* FMaps: various updates (mostly suggested by P. Casteran)Gravatar letouzey2008-12-26
| | | | | | | | | | | | | - New functions: update (a kind of union), restrict (a kind of inter), diff. - New predicat Partition (and Disjoint), many results about Partition. - Equivalence instead of obsolete Setoid_Theory (they are aliases). refl_st, sym_st, trans_st aren't used anymore and marked as obsolete. - Start using Morphism (E.eq==>...) instead of compat_... This change (FMaps only) is incompatible with 8.2betaX, but it's really better now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11718 85f007b7-540e-0410-9357-904b9bb8a0f7
* FMap: fold_rec + more permissive transpose hyp + various cleanupGravatar letouzey2008-12-22
| | | | | | | The induction principles for fold are due to S. Lescuyer The better transpose hyp is a suggestion by P. Casteran git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11711 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
* Integration of theories/Ints into theories/Numbers, part 1: moving filesGravatar letouzey2008-05-07
| | | | | | | | | | | | | | For the moment, the Ints files are simply moved into directories in theories/Numbers with meaningful names. No filenames changed, apart from: Zaux.v -> theories/Numbers/BigNumPrelude.v MemoFn.v -> theories/Lists/StreamMemo.v More to come... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10899 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
* migration from Set to Type of FSet/FMap + some dependencies...Gravatar letouzey2008-03-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10616 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
* Added ForAll_Str_nth_tlGravatar roconnor2007-07-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9967 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Extensions of FMap(Weak)Facts: Gravatar letouzey2007-06-27
| | | | | | | | | | | | | | | fold properties and induction principles for (weak) maps. - Simplification in SetoidList: the two important results fold_right_equivlistA and fold_right_add are now proved without using removeA and hence do not depend anymore on a decidable equality (good for maps and their arbitrary datas). In fact, removeA is not used at all anymore, but I leave it here (mostly), since it can't hurt. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9914 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added zwqipWith.Gravatar roconnor2007-06-26
| | | | | | | Added theory about intractions between nth and map, and zipWith. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9909 85f007b7-540e-0410-9357-904b9bb8a0f7
* additional properties for FMap (and slight rework of SetoidList and ↵Gravatar letouzey2007-06-26
| | | | | | FSetProperties) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9908 85f007b7-540e-0410-9357-904b9bb8a0f7
* oups: one file forgotten in my previous commitGravatar letouzey2007-06-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9891 85f007b7-540e-0410-9357-904b9bb8a0f7
* some more properties of fold and elements in FSetPropertiesGravatar letouzey2007-06-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9885 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1510Gravatar notin2007-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9777 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1499Gravatar notin2007-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9767 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement dans le kernel : Gravatar bgregoir2006-12-11
| | | | | | | | | | | | | | | | | | | | | - essai de suppression des dependances debiles. (echec) - Application des patch debian. Pour ring et field : - introduciton de la function de sign et de puissance. - Correction de certains bug. - supression de ring_replace .... Pour exact_no_check : - ajout de la tactic : vm_cast_no_check (t) qui remplace "exact_no_check (t<: type of Goal)" (cette version forcais l'evaluation du cast dans le pretypage). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9427 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
* Changement de précédence de l'argument du by de assert; ↵Gravatar herbelin2006-05-23
| | | | | | conséquences sur les .v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8853 85f007b7-540e-0410-9357-904b9bb8a0f7
* un debut de propriétés concernant FMapGravatar letouzey2006-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8844 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 16:27:09 +0000