aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Collapse)AuthorAge
* Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl)Gravatar herbelin2009-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11990 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
* Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"Gravatar herbelin2009-03-16
| | | | | | | | | | | | | | now works correctly, "unfold foo at 4 in H at 3" now fails correctly, etc.). The terminology for clauses (though I don't find the term "clause" very intuitive after all) is mostly preserved except for "simple_clause" which becomes a light form of "clause" instead of being an atom of clause (what played the role of "simple_clause" is now called "goal_location" - better names are welcome). Main changes are in tacticals.ml and tactics.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11981 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning/uniformizing the interface of tacticals.mliGravatar herbelin2009-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11980 85f007b7-540e-0410-9357-904b9bb8a0f7
* illegal tactic application was having Ltac interpreter loopGravatar barras2009-03-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11963 85f007b7-540e-0410-9357-904b9bb8a0f7
* commande Timeout + compaction des traces de debug_tacticGravatar barras2009-03-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11959 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack sur la mémoïsation de nf_evar.Gravatar aspiwack2009-03-04
| | | | | | | | | | | | | | | | L'expérience prouve que ce n'est pas franchement concluant. On peut se risquer à une explication : - nf_evar, version mémoïsée n'est pas tail recursive - On retarde la substitution des hypothèses de l'evar en échange de faire moins de substitutions d'evars. Intuitivement c'est intéressant seulement si il y a plus de substitutions d'evar dupliquées que d'hypothèses dupliquées. Ce qui ne doit pas être le cas (ne serait-ce que parce que dupliquer une evar duplique aussi ses variables libres). This reverts commit 066a564021788e995eb166ad6ed6e55611d6f593. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11958 85f007b7-540e-0410-9357-904b9bb8a0f7
* =?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et ↵Gravatar aspiwack2009-02-27
| | | | | | | | | | | | | | | | | | | | =20[whd=5Fevar]=20:=20les =20evar=5Fdefs=20gardent=20un=20cache=20des=20appels=20pr=C3=A9c=C3=A9dents.=20Le=20d=C3=A9faut=20de=20la =20m=C3=A9thodologie=20est=20que=20=C3=A7a=20int=C3=A9ragit=20assez=20mal=20avec=20la=20substitution=20des =20hypoth=C3=A8ses=20de=20l'evar=20(qui=20n'est=20pas=20mise=20en=20cache).=20En=20particulier=20les =20deux=20fonctions=20ne=20sont=20plus=20r=C3=A9cursives=20terminales.=20De=20plus=20un=20appel=20=C3=A0 =20l'une=20des=20deux=20fera=20n=C3=A9cessairement=20un=20parcours=20du=20terme=20pour=20appliquer =20la=20substitution.?= MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit D'un point de vue de l'effet observer, ça a un effet assez léger sur le trunk, je suis curieux de voir les effets sur les contribs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11950 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add support for dependent "destruct" over terms in dependent types.Gravatar herbelin2009-02-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11944 85f007b7-540e-0410-9357-904b9bb8a0f7
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | par Evd). Ça s'accompagne de quelques autres modifications de l'interface (certaines fonctions étaient des doublons, ou des conversions entre evar_map et evar_defs). J'ai modifié un peu la structure de evd.ml aussi, pour éviter des fonctions redéfinies deux fois (i.e. définies trois fois !), j'ai introduit des sous-modules pour les différentes couches. Il y a à l'heure actuelle une pénalité en performance assez sévère (due principalement à la nouvelle mouture de Evd.merge, si mon diagnostique est correct). Mais fera l'objet de plusieurs optimisations dans les commits à venir. Un peu plus ennuyeux, la test-suite du mode déclaratif ne passe plus. Un appel de Decl_proof_instr.mark_as_done visiblement, je suis pour l'instant incapable de comprendre ce qui cause cette erreur. J'espère qu'on pourra le déterminer rapidement. Ce commit est le tout premier commit dans le trunk en rapport avec les évolution futures de la machine de preuve, en vue en particulier d'obtenir un "vrai refine". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11939 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix [apply_in] which short-circuited resolution of evars in a customGravatar msozeau2009-02-16
| | | | | | | [clenv_refine] (bug reported by B. Gregoire). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11927 85f007b7-540e-0410-9357-904b9bb8a0f7
* pushed evar reduction in kernelGravatar barras2009-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11889 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report r11631 from 8.2 and handle non-dependent goals better inGravatar msozeau2009-02-04
| | | | | | | [dependent induction]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11881 85f007b7-540e-0410-9357-904b9bb8a0f7
* Solves some warning and hides some not-bad ones in doc. It remains aGravatar herbelin2009-01-29
| | | | | | | | | few hevea warning (failure to put a vector on an expression in Classes.tex, failure to support multirow in RecTutorial.tex). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11868 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petit nettoyage faisant suite au commit #11847 .Gravatar aspiwack2009-01-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | Quelques modifications autour (géographiquement) de Util.list_split_at Util.list_split_at devient Util.list_split_when (dénomination inventée arbitrairement par moi-même, mais qui ne devrait pas déranger grand monde vu qu'il semble n'y avoir que deux occurences de cette fonction). Pour laisser la place à la fonction suivante : Introduction de Util.list_split_at: qui sépare la liste à une position donnée (alors que la nouvellement nommé list_split_when sépare à la première occurence "vrai" d'un prédicat). Ajout de quelques commentaires dans util.ml (pas le mli) sur ces deux fonctions. Suppression de Impargs.list_split_at (appel à Util). Suppression de Subtac_pretyping.list_split_at (qui était du code mort de toute façon). Suppression Util.list_split_by qui n'est utilisé nulle part et est une réimplémentation de List.partition (qui est probablement meilleure, en particulier tail-recursive) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11851 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2004 due to bad handling of evars in the unification for Gravatar msozeau2009-01-21
| | | | | | | the setoid_rewrite variant called by rewrite (bug traced by Hugo). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11822 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
* Getting rid of the previous implementation of setoid_rewrite which wasGravatar msozeau2009-01-18
| | | | | | | unplugged a long time ago. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11798 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix a bunch of bugs related to setoid_rewrite, unification and evars:Gravatar msozeau2009-01-12
| | | | | | | | | | | | - Really unify with types of metas when they contain metas _or_ evars (why not always?) (fixes bug #2027). - Better handling of evars in rewrite lemmas when using setoid_rewrite through rewrite (reported by Ralf Hinze). - Use retyping with metas when possible (check?) and improve an obscure error message in retyping. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11776 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Deactivation of dynamic loading on Mac OS 10.5 (see bug #2024).Gravatar herbelin2009-01-11
| | | | | | | | | | | | - Added dependency of mltop.ml4 into config/Makefile (see bug #2023). - Fixed bug #1963 (dependent inversion building a universe-ill-formed conversion problem). - Incidentally, moved "Large non-propositional inductive ..." error message to standard himsg.ml error displayer. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11774 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bugs #2001 (search_guard was overwriting the guard index givenGravatar herbelin2009-01-04
| | | | | | | | by user) and #2017 (unification pattern test too crude leading to regression wrt to 8.1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11743 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed two problems:Gravatar herbelin2009-01-03
| | | | | | | | | - Function descend_in_conjunctions was now too weak, use match_with_record. - Added documentation of new notation for destruct with equation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11742 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Temptative change to notations like "as [|n H]_eqn" or "as [|n H]_eqn:H",Gravatar herbelin2009-01-02
| | | | | | | | | and, with a now generic intropattern "[]", also "as []_eqn", "as []_eqn:H" for "destruct" with equality keeping. - Fixed an accuracy loss in error location. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11732 85f007b7-540e-0410-9357-904b9bb8a0f7
* Switched to "standardized" names for the properties of eq andGravatar herbelin2009-01-01
| | | | | | | | | identity. Add notations for compatibility and support for understanding these notations in the ml files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11729 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
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
| | | | | | | | | | splay_prod_n, lam_it -> it_mkLambda, splay_lambda -> splay_lam). Added shortcuts for "fst (decompose_prod t)" and co. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11727 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixed bugs and compatibilities issues in Gravatar herbelin2008-12-30
| | | | | | | | | | match_conjunction/match_disjunction/array_for_all_i - Finally activate fine-tuned unfolding of iff in tauto: it breaks at only one place in the user contribs (FSetAVL_dep.v). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11726 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
| | | | | | | | | | | | | - Backtrack on precise unfolding of "iff" in "tauto": it has effects on the naming of hypotheses (especially when doing "case H" with H of type "{x|P<->Q}" since not unfolding will eventually introduce a name "i" while unfolding will eventually introduce a name "a" (deep sigh). - Miscellaneous (error when a plugin is missing, doc hnf, standardization of names manipulating type constr_pattern, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11725 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
* - Extracted from the tactic "now" an experimental tactic "easy" for smallGravatar herbelin2008-12-26
| | | | | | | | | | | | | | | | | automation. - Permitted to use evars in the intermediate steps of "apply in" (as expected in the test file apply.v). - Back on the systematic use of eq_rect (r11697) for implementing rewriting (some proofs, especially lemma DistOoVv in Lyon/RulerCompassGeometry/C14_Angle_Droit.v and tactic compute_vcg in Sophia-Antipolis/Semantics/example2.v are explicitly refering to the name of the lemmas used for rewriting). - Fixed at the same time a bug in get_sort_of (predicativity of Set was not taken into account). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11717 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Optimized "auto decomp" which had a (presumably) exponential inGravatar herbelin2008-12-26
| | | | | | | | | the number of conjunctions to split. - A few cleaning and uniformisation in auto.ml. - Removal of v62 hints already in core. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11715 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixed cutrewrite bug #2021 introduced in commit 11662 (as a sideGravatar herbelin2008-12-18
| | | | | | | | | | | | | | | effect, old cut_replacing was betaiota-normalizing, new cut_replacing, from commit 11662, does not; turn betaiota-normalisation into a purer and simpler whd_beta of the abstracted rewriting predicate to the rewritten term). - Made "induction in" more flexible when induction is on a goal variable (accept occurrences -- even if theoretically unnecessary -- so as e.g. not to expand occurrences that would otherwise trigger reductions - see example in Peano.mult_succ_r). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11697 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finish fix for the treatment of [inverse] in [setoid_rewrite], making aGravatar msozeau2008-12-16
| | | | | | | | | | variant of the [unify] tactic that takes a hint db as argument and does unification modulo its [transparent_state]. Add test-file for bug #1939 and another [AdvancedTypeClasses.v] that mimicks [AdvancedCanonicalStructure.v]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11685 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix looping class resolution bug discovered by B. Aydemir and use theGravatar msozeau2008-12-14
| | | | | | | | right unification flags for exact hints in eauto (may break a lot of things by succeeding much more often). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11681 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed in bug in previous 11662 (incorrect with_evars flag in ↵Gravatar herbelin2008-12-12
| | | | | | descend_conjunction) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11670 85f007b7-540e-0410-9357-904b9bb8a0f7
* About "apply in":Gravatar herbelin2008-12-09
| | | | | | | | | | | | | | | | | | - Added "simple apply in" (cf wish 1917) + conversion and descent under conjunction + contraction of useless beta-redex in "apply in" + support for open terms. - Did not solve the "problem" that "apply in" generates a let-in which is type-checked using a kernel conversion in the opposite side of what the proof indicated (hence leading to a potential unexpected penalty at Qed time). - When applyng a sequence of lemmas, it would have been nice to allow temporary evars as intermediate steps but this was too long to implement. Smoother API in tactics.mli for assert_by/assert_as/pose_proof. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11662 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do not catch _all_ exceptions in setoid unification.Gravatar msozeau2008-12-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11658 85f007b7-540e-0410-9357-904b9bb8a0f7
* closed bug 1898: fold x in x; added a reordering primitive tacticGravatar barras2008-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11632 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fine-tuning rewriting from "eq_true b": using <- to rewrite true to bGravatar herbelin2008-11-23
| | | | | | | (if ever necessary). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11621 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixed minor bug #1994 in the tactic chapter of the manual [doc]Gravatar herbelin2008-11-22
| | | | | | | | | | | | | - Improved warning when found several path to the same file in path [mltop.ml4, system.ml] - Add support for "rewrite" on specific equality to true (i.e. eq_true) [Datatypes.v, tactics] PS: compilation test made over 11611 to shunt the archive-breaking 11612 and 11614 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11617 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug reported by Mark Dickinson on Coq-Club about [setoid_rewrite] notGravatar msozeau2008-11-10
| | | | | | | reducing the type of the given lemma. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11571 85f007b7-540e-0410-9357-904b9bb8a0f7
* More factorization of inductive/record and typeclasses: move classGravatar msozeau2008-11-09
| | | | | | | | | | | | declaration code to toplevel/record, including support for singleton classes as definitions. Parsing code also factorized. Arnaud: one more thing to think about when refactoring the definitions in vernacentries. Add support for specifying what to do with anonymous variables in contexts during internalisation (fixes bug #1982), current choice is to generate a name for typeclass bindings. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11563 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixed bug 1968 (inversion failing due to a Not_found bug introduced inGravatar herbelin2008-11-09
| | | | | | | | | | | | Evarutil.check_and_clear_in_constr in V8.2 revision 11309 and trunk revision 11300). - Improved various error messages related to inversion, evars and case analysis (including the removal of the obsolete dependent/non dependent distinction). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11561 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add the ability to give a specific tactic to solve each obligation inGravatar msozeau2008-11-07
| | | | | | | Program. No syntax to do it yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11550 85f007b7-540e-0410-9357-904b9bb8a0f7
* Port [rewrite] tactics to open terms. Currently no check that evarsGravatar msozeau2008-11-05
| | | | | | | | introduced by the lemma remain in the subgoals (i.e. it's really [erewrite]). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11544 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adaptation to ocaml 3.11 new semantics of String.index_from (see bug #1974)Gravatar herbelin2008-11-04
| | | | | | | Grant wish #1988 ("fun" forces reduction in "refine" if needed) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11536 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adaptation du vieil appel à "apply" sur lemme de symétrie au cas oùGravatar herbelin2008-10-29
| | | | | | | | | | | | une réduction a eu lieu (insertion d'un "change" pour que "apply" n'échoue pas). À faire : nettoyer la construction par tactique de la preuve de symétrie de a=b -> b=a (quand le lemme de symétrie n'existe pas) pour quelle ne lance pas une conversion potentiellement longue entre a et b (le cas est arrivé dans CatsInZFC/notation.v !) [HH + MS] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11521 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
* Fixes and refinements regarding occurrence selection:Gravatar herbelin2008-10-26
| | | | | | | | | | | | | | | - make the modifiers "value of" and "type of" for "set" working (it was not!), - clear unselected hypotheses in the "in" clause of "induction/destruct" when the destructed term is a variable (experimental), - support for generalization of hypotheses in the induction hypotheses using the "in" clause of "induction" (e.g. "induction n in m, H" will generalize over m -- would it be better to have an explicit "over"/"generalizing" clause ?). Added clause "as" to "apply in". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11509 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack sur commit 11467 (tentative d'optimisation meta_instance quiGravatar herbelin2008-10-26
| | | | | | | | | s'est avéré ralentir la compilation des user-contribs au final, sans compter aussi le bug 1980 apparemment introduit par ce commit). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11505 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-09 12:06:29 +0000