aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Arith
Commit message (Collapse)AuthorAge
* DecidableType: A specification via boolean equality as an alternative to eq_decGravatar letouzey2009-11-10
| | | | | | + adaptation of {Nat,N,P,Z,Q,R}_as_DT for them to provide both eq_dec and eqb git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12488 85f007b7-540e-0410-9357-904b9bb8a0f7
* Better visibility of the inductive CompSpec used to specify comparison functionsGravatar letouzey2009-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12462 85f007b7-540e-0410-9357-904b9bb8a0f7
* OrderedType implementation for various numerical datatypes + min/max structuresGravatar letouzey2009-11-03
| | | | | | | | | | | | | | | | | | | | | | | | - A richer OrderedTypeFull interface : OrderedType + predicate "le" - Implementations {Nat,N,P,Z,Q}OrderedType.v, also providing "order" tactics - By the way: as suggested by S. Lescuyer, specification of compare is now inductive - GenericMinMax: axiomatisation + properties of min and max out of OrderedTypeFull structures. - MinMax.v, {Z,P,N,Q}minmax.v are specialization of GenericMinMax, with also some domain-specific results, and compatibility layer with already existing results. - Some ML code of plugins had to be adapted, otherwise wrong "eq", "lt" or simimlar constants were found by functions like coq_constant. - Beware of the aliasing problems: for instance eq:=@eq t instead of eq:=@eq M.t in Make_UDT made (r)omega stopped working (Z_as_OT.t instead of Z in statement of Zmax_spec). - Some Morphism declaration are now ambiguous: switch to new syntax anyway. - Misc adaptations of FSets/MSets - Classes/RelationPairs.v: from two relations over A and B, we inspect relations over A*B and their properties in terms of classes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12461 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
* A few additions in Min.v.Gravatar herbelin2009-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12368 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
* Better comparison functions in OrderedTypeExGravatar letouzey2009-07-22
| | | | | | | | | | | | | | | The compare functions are still functions-by-tactics, but now their computational parts are completely pure (no use of lt_eq_lt_dec in nat_compare anymore), while their proofs parts are simply calls to (opaque) lemmas. This seem to improve the efficiency of sets/maps, as mentionned by T. Braibant, D. Pous and S. Lescuyer. The earlier version of nat_compare is now called nat_compare_alt, there is a proof of equivalence named nat_compare_equiv. By the way, various improvements of proofs, in particular in Pnat. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12247 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some additions in Max and Zmax. Unifiying list of statements and namesGravatar herbelin2009-04-14
| | | | | | | | in both files. Late update of CHANGES wrt classical Tauto. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12084 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixed bug #2021 (uncaught exception with injection/discriminate whenGravatar herbelin2009-01-01
| | | | | | | | | | | | the inductive status of a projectable position comes from a dependency). - Improved doc of the stdlib chapter (see bug #2018), and fixed tex bugs introduced in r11725. - Applied wish #2012 (max_dec transparent). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11728 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Another bug in get_sort_family_of (sort-polymorphism of constants andGravatar herbelin2008-12-28
| | | | | | | | | | | | | | | | | | | | | | | inductive types was not taken into account). - Virtually extended tauto to - support arbitrary-length disjunctions and conjunctions, - support arbitrary complex forms of disjunctions and conjunctions when in the contravariant of an implicative hypothesis, - stick with the purely propositional fragment and not apply reflexivity. This is virtual in the sense that it is not activated since it breaks compatibility with the existing tauto. - Modified the notion of conjunction and unit type used in hipattern in a way that is closer to the intuitive meaning (forbid dependencies between parameters in conjunction; forbid indices in unit types). - Investigated how far "iff" could be turned into a direct inductive definition; modified tauto.ml4 so that it works with the current and the alternative definition. - Fixed a bug in the error message from lookup_eliminator. - Other minor changes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11721 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixed many "Theorem with" bugs.Gravatar herbelin2008-10-27
| | | | | | | | | | | - Fixed doc of assert as. - Doc of apply in + update credits. - Nettoyage partiel de Even.v en utilisant "Theorem with". - Added check that name is not in use for "generalize as". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11511 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tentative de relecture des scripts de Mult.v au regard des tactiques actuellesGravatar herbelin2008-07-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11224 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
| | | | | | | | | | | | | | | | | - Ajout clause "in" à "remember" (et passage du code en ML). - Ajout clause "in" à "induction"/"destruct" qui, en ce cas, ajoute aussi une égalité pour se souvenir du terme sur lequel l'induction ou l'analyse de cas s'applique. - Ajout "pose t as id" en standard (Matthieu: j'ai enlevé celui de Programs qui avait la sémantique de "pose proof" tandis que le nouveau a la même sémantique que "pose (id:=t)"). - Un peu de réorganisation, uniformisation de noms dans Arith, et ajout EqNat dans Arith. - Documentation tactiques et notations de tactiques. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11072 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Modification de la déf de minus et pred conformément aux remarques deGravatar herbelin2008-05-28
| | | | | | | | | | | Assia et Benjamin W. de telle sorte qu'ils respectent le critère de décroissance structurelle lorsqu'utilisés dans un point-fixe. - Ajout des noms "standard" des lemmes de Peano et correction d'un nom de BinInt. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11015 85f007b7-540e-0410-9357-904b9bb8a0f7
* Une passe sur les réels:Gravatar herbelin2008-03-23
| | | | | | | | | | | | | | | | | | | | | | | | - Renommage de Rlt_not_le de Fourier_util en Rlt_not_le_frac_opp pour éviter la confusion avec le Rlt_not_le de RIneq. - Quelques variantes de lemmes en plus dans RIneq. - Déplacement des énoncés de sigT dans sig (y compris la complétude) et utilisation de la notation { l:R | }. - Suppression hypothèse inutile de ln_exists1. - Ajout notation ² pour Rsqr. Au passage: - Déplacement de dec_inh_nat_subset_has_unique_least_element de ChoiceFacts vers Wf_nat. - Correction de l'espace en trop dans les notations de Specif.v liées à "&". - MAJ fichier CHANGES Note: il reste un axiome dans Ranalysis (raison technique: Ltac ne sait pas manipuler un terme ouvert) et dans Rtrigo.v ("sin PI/2 = 1" non prouvé). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10710 85f007b7-540e-0410-9357-904b9bb8a0f7
* even_2n et odd_S2n deviennent transparents (chez moi, ça empêchait de ↵Gravatar notin2008-03-06
| | | | | | compiler la contrib Nijmegen/QArith ?!) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10625 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack sur la révision #10401 : suppression de le_minus de la base de ↵Gravatar notin2008-03-05
| | | | | | hints arith git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10621 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
* Deux petits théorèmes utiles dans Minus.vGravatar notin2007-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10401 85f007b7-540e-0410-9357-904b9bb8a0f7
* Corrected the ML code for well-founded recursion in the comment.Gravatar emakarov2007-11-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10306 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
* Changement esthétique de la preuve de mult_is_oneGravatar notin2007-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10274 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de lemmes d'inversion pour mult (sur le modèle de plus_is_O et ↵Gravatar notin2007-10-30
| | | | | | plus_is_one) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10273 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deletion of an obsolete file (euclidian division done in old syntax with ↵Gravatar letouzey2007-07-12
| | | | | | realizers) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9987 85f007b7-540e-0410-9357-904b9bb8a0f7
* Big reorganization of romega/ReflOmegaCore.v: towards a modular Gravatar letouzey2007-07-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | and generic romega tactic... For the moment, nothing is visible yet from the user's point of view (hopefully). But internally, we prepare a romega that can works on any integer types. ReflOmegaCore is now separated in several modules: * First, an interface Int that specifies the minimal amount of things needed on our integer type for romega to work: - int should be a ring (re-use of ring_theory definition ;-) - it should come with an total order, compatible with + * - - we should have a decidable ternary comparison function - moreover, we ask one (and only one!) critical property specific to integers: a<b <-> a<=b-1 * Then a functor IntProperties derives from this interface all the various lemmas on integers that are used in the romega part, in particular the famous OMEGA?? lemmas. * The romega reflexive part is now in another functor IntOmega, that rely on some Int: no more Z inside. The main changes is that Z0 was a constructor whereas our abstract zero isn't. So matching Z0 is transformed into (if beq ... 0 then ...). With extensive use of && and if then else, it's almost clearer this way. * Finally, for the moment Z_as_Int show that Z fulfills our interface, and ZOmega = IntOmega(Z_as_Int) is used by the tactic. Remains to be done: - revision of the refl_omega to use any Int instead of just Z, and creating a user interface. - Int has no particular reason to use the leibniz equality (only rely on the beq boolean test). Setoids someday ? - a version with "semi-ring" for nat ? or rather a generic way to plug additional equations on the fly, e.g. n>=0 for every nat subpart ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9966 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension of NArith: Nminus, Nmin, etcGravatar letouzey2007-06-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9883 85f007b7-540e-0410-9357-904b9bb8a0f7
* simplier version of tail_plusGravatar letouzey2007-04-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9750 85f007b7-540e-0410-9357-904b9bb8a0f7
* Proof simplification for eq_nat_dec et le_lt_dec: induction over Gravatar letouzey2007-03-12
| | | | | | | | | 2nd arg m can simply be a destruct. This helps (vm_)compute __a lot__. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9698 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajouts de lemmes dans Min et MaxGravatar notin2007-02-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9660 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixes PR#1269 about function: there is no reason well founded induction isGravatar bertot2006-11-05
| | | | | | limited to only Set and not any type in Type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9340 85f007b7-540e-0410-9357-904b9bb8a0f7
* simplif de la partie ML de ring/fieldGravatar barras2006-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9302 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en forme des theoriesGravatar notin2006-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout du théorème mult_minus_distr_lGravatar notin2006-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9237 85f007b7-540e-0410-9357-904b9bb8a0f7
* Arith NArith et ZArith exportent ring + nettoyage dans Ring_polynomGravatar barras2006-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9210 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵Gravatar notin2006-04-28
| | | | | | 'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un gros coup de lifting pour IntMap: Gravatar letouzey2006-04-25
| | | | | | | | | | | | | | | | | | | | | | * le type ad des adresses est maintenant un alias vers le N de NArith, qui lui est isomorphe. * toutes les operations sur ces adresses (p.ex. un xor bit a bit) sont maintenant dans de nouveaux fichiers du repertoire NArith. * Intmap utilise maintenant le meme type option que le reste du monde * etc etc... Tout ceci ne preserve pas forcement la compatibilite. Les 4 contribs utilisant Intmap sont adaptees en consequence. Me demander si besoin ma moulinette d'adaptation (incomplete). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8733 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
* Unification max_case et max_case2Gravatar herbelin2006-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8030 85f007b7-540e-0410-9357-904b9bb8a0f7
* Unification min_case et min_case2Gravatar herbelin2006-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8029 85f007b7-540e-0410-9357-904b9bb8a0f7
* Application du souhait de transparence de well_founded_ltof (#1007)Gravatar herbelin2005-12-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7766 85f007b7-540e-0410-9357-904b9bb8a0f7
* legere simplification des preuves de le_S_n et pred_leGravatar letouzey2005-02-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6669 85f007b7-540e-0410-9357-904b9bb8a0f7
* compatibility with POWERPCGravatar gregoire2004-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6338 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement dans les boxed values .Gravatar gregoire2004-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
* TypoGravatar herbelin2004-08-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6010 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
* Nouveaux thms de non circularité de natGravatar herbelin2004-06-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5795 85f007b7-540e-0410-9357-904b9bb8a0f7
* ide: silent behavior better, save icon, -byte worksGravatar marche2004-03-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5427 85f007b7-540e-0410-9357-904b9bb8a0f7
* modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesGravatar barras2003-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5099 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 14:29:47 +0000