aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Collapse)AuthorAge
* DISCLAIMERGravatar puech2009-01-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ========== This big patch is commited here with a HUGE experimental tag on it. It is probably not a finished job. The aim of committing it now, as agreed with Hugo, is to get some feedback from potential users to identify more clearly the directions the implementation could take. So please feel free to mail me any remarks, bug reports or advices at <puech@cs.unibo.it>. Here are the changes induced by it : For the user ============ * Search tools have been reimplemented to be faster and more general. Affected are [SearchPattern], [SearchRewrite] and [Search] (not [SearchAbout] yet). Changes are: - All of them accept general constructions, and previous syntactical limitations are abolished. In particular, one can for example [SearchPattern (nat -> Prop)], which will find [isSucc], but also [le], [gt] etc. - Patterns are typed. This means that you cannot search mistyped expressions anymore. I'm not sure if it's a good or a bad thing though (especially regarding coercions)... * New tool to automatically infer (some) Record/Typeclasses instances. Usage : [Record/Class *Infer* X := ...] flags a record/class as subject to instance search. There is also an option to activate/deactivate the search [Set/Unset Autoinstance]. It works by finding combinations of definitions (actually all kinds of objects) which forms a record instance, possibly parameterized. It is activated at two moments: - A complete search is done when defining a new record, to find all possible instances that could have been formed with past definitions. Example: Require Import List. Record Infer Monoid A (op:A->A->A) e := { assoc : forall x y z, op x (op y z) = op (op x y) z; idl : forall x, x = op x e ; idr : forall x, x = op e x }. new instance Monoid_autoinstance_1 : (Monoid nat plus 0) [...] - At each new declaration (Definition, Axiom, Inductive), a search is made to find instances involving the new object. Example: Parameter app_nil_beg : forall A (l:list A), l = nil ++ l. new instance Build_Monoid_autoinstance_12 : (forall H : Type, Monoid (list H) app nil) := (fun H : Type => Build_Monoid (list H) app nil ass_app (app_nil_beg H) (app_nil_end H)) For the developper ================== * New yet-to-be-named datastructure in [lib/dnet.ml]. Should do efficient one-to-many or many-to-one non-linear first-order filtering, faster than traditional methods like discrimination nets (so yes, the name of the file should probably be changed). * Comes with its application to Coq's terms [pretyping/term_dnet.ml]. Terms are represented so that you can search for patterns under products as fast as you would do not under products, and facilities are provided to express other kind of searches (head of application, under equality, whatever you need that can be expressed as a pattern) * A global repository of all objects defined and imported is maintained [toplevel/libtypes.ml], with all search facilities described before. * A certain kind of proof search in [toplevel/autoinstance.ml]. For the moment it is specialized on finding instances, but it should be generalizable and reusable (more on this in a few months :-). The bad news ============ * Compile time should increase by 0 to 15% (depending on the size of the Requires done). This could be optimized greatly by not performing substitutions on modules which are not functors I think. There may also be some inefficiency sources left in my code though... * Vo's also gain a little bit of weight (20%). That's inevitable if I wanted to store the big datastructure of objects, but could also be optimized some more. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11794 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correct a bug in commit 11659Gravatar puech2009-01-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11792 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
* Completed 11745 (move of jprover to user contribs) and cleaned 11743Gravatar herbelin2009-01-05
| | | | | | | | (detection of Miller's pattern) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11748 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 apparent inconsistencies in matching.ml:Gravatar herbelin2009-01-02
| | | | | | | | | | | | - matching_subterm was activating partial_app to true in matches_core even when no partial_app was expected, - "match goal" (hence "extended_matches") was called with partial_app in 8.2 (currently "matches" but not in trunk; what to do with (legacy) "matches" remains unclear. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11733 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
* - 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
* Fix exponential behaviour of the typeclasses persistent objects. DropGravatar puech2008-12-06
| | | | | | | | | unused methods object. Matthieu please review this change (after monday), I might have introduced a bug in rebuild_instance. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11659 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes for unification and substitution of metas under binders.Gravatar msozeau2008-12-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11655 85f007b7-540e-0410-9357-904b9bb8a0f7
* improved simplGravatar barras2008-12-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11653 85f007b7-540e-0410-9357-904b9bb8a0f7
* Miscellaneous fixes and improvements:Gravatar herbelin2008-12-02
| | | | | | | | | | | - Fixed a virtual bug of unification (ever occurs if w_unify called with a non-empty context of rel's, which is a priori uncommon). - Fixed Notation.out test. - Add better coqide error message in case editor is called on an unnamed file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11650 85f007b7-540e-0410-9357-904b9bb8a0f7
* another bug with simplGravatar barras2008-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11644 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix (?) a pattern matching compilation problem: Gravatar msozeau2008-11-27
| | | | | | | | | | | | | | | | | << Axiom A : nat -> bool. Definition foo := match A 0 with | true => true | k => k end. Print foo. >> [A 0] is duplicated in the [k => k] branch! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11640 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed bug 1791: simpl was performing eta expansionGravatar barras2008-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11636 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixing problem with CompCert: reordering resulting from tac change was not ↵Gravatar barras2008-11-27
| | | | | | closed w.r.t. dependencies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11634 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed problem with r11612Gravatar barras2008-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11614 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed exponential behavior of evar unif (ground case)Gravatar barras2008-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11612 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restores behaviour of v8.1 for unification problems which fail (backport of ↵Gravatar letouzey2008-11-14
| | | | | | 11585) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11590 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
* Apply vmconv if there are no _undefined_ evars around.Gravatar msozeau2008-11-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11560 85f007b7-540e-0410-9357-904b9bb8a0f7
* Slight change of the semantics of user-given casts: they don't reallyGravatar msozeau2008-11-07
| | | | | | | | | | | | | | | | | help the type _checking_ anymore (they don't become typing constraints) but they permit to coerce a subterm in a type. In particular, when using a VM cast we avoid unneeded, unexpected conversions using the default machine (oops!). Also remove the corresponding comment in pretyping and fix the wrong use of casts in toplevel/command: accept the trouble of using evars. This has the somewhat adverse effect that when typing casted object we now have no typing constraints (see e.g. examples in Cases.v)! Probably, this will be backtracked partially tomorrow as many contribs can rely on it and the change could make some unifications fail (in particular with deep coercions). Let's try anyway! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11558 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix universe problem appearing ConCaT using the existing infrastructure forGravatar msozeau2008-11-07
| | | | | | | | | | declaring additional conversion problems when unifying the type of an evar instance and the evar's declared type. Fix the corresponding conversion heuristic which failed due to (misplaced?) assertions when faced with general conversion problems. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11549 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix in the unification algorithm using evars: unify types of evarGravatar msozeau2008-11-05
| | | | | | | | | | | | instances and the corresponding evar's type if it contains existentials to avoid dangling evars. No noticeable performance impact (at least on the stdlib). Subsumes (and fixes) the (broken) fix in unification.ml that was previously patched by M. Puech. Improve error messages related to existential variables and type classes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11543 85f007b7-540e-0410-9357-904b9bb8a0f7
* Move Record desugaring to constrintern and add ability to use notationsGravatar msozeau2008-11-05
| | | | | | | | | for record fields (using "someproj : sometype where not := constr" syntax). Only one notation allowed currently and no redeclaration after the record declaration either (will be done for typeclasses). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11542 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
* More debugging of handling of open constrs with typeclasses:Gravatar msozeau2008-10-25
| | | | | | | | avoid trying to resolve classes early in open constr arguments for Ltac, the tactics themselves should do whatever's appropriate with the constraints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11503 85f007b7-540e-0410-9357-904b9bb8a0f7
* Open notation for declaring record instances.Gravatar msozeau2008-10-23
| | | | | | | | | | | | | | | | | | | | It solves feature request 1852, makes me and Arnaud happy and will permit to factor some more code in typeclasses. - Records are introduced using the syntax "{| x := t; y := foo |}" and "with" clauses are currently parsed but not yet supported in the elaboration. You are invited to suggest other syntaxes :) - Missing fields are turned into holes, extra fields cause an error message. The current implementation finds the type of the record at pretyping time, from the typing constraint alone (and just expects an inductive with one constructor). It is then impossible to use scope information to parse the bodies: that may be wrong. The other solution I see is using the fields to detect the type earlier, before internalisation of the bodies, but then we get in name clash hell. - In funind/contrib/interface I mostly put [assert false] everywhere to avoid warnings. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11496 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retour en arrière pour raison de compatibilité sur la suppression du nf_evar Gravatar herbelin2008-10-19
| | | | | | | | | | | | | | | | | | dans clos_norm_flags (cf échec dans CoRN.Transc.InvTrigonom.Tan_ilim). Ceci dit : - cela ne me parait pas moral que clos_norm_flags s'occupe de normaliser les evars, - mais comme "evar" n'est pas un flag supporté par closure.ml, on ne peut pas le donner à la demande comme argument de clos_norm_flags (question: pourrait-on faire supporter la réduction Evar par closure.ml ??). Plus généralement, il y a un problème avec la propagation des instantiations des evars à travers les buts (cf lemme eapply_evar dans test-suite/success/apply.v). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11470 85f007b7-540e-0410-9357-904b9bb8a0f7
* Optimisation de clenv.ml pour que meta_instance ne soit pas appeléGravatar herbelin2008-10-18
| | | | | | | | | | abusivement sur les clauses. Nettoyage au passage de metamap qui était utilisé à la fois pour les substitutions de meta et pour les contextes de typage de meta. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11467 85f007b7-540e-0410-9357-904b9bb8a0f7
* * Fixed constr_cmp again to handle universes subtyping correctlyGravatar puech2008-10-09
| | | | | | | | | | * Fixed typo in unify_0 regarding conv_pb * First attempt to fix a problem related to rels in w_merge. Seems to be unsuccessful at this point git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11443 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixing r11433 again:Gravatar barras2008-10-07
| | | | | | | | | | | | | - backtrack on kernel modifications: the monomorphic instance of an inductive type is constrained to live in an universe higher (or equal) than all the instances - improved support for polymorphic inductive types at the refiner level: introduced type_of_inductive_knowing_conclusion that computes the instance to match the current conclusion universe. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11435 85f007b7-540e-0410-9357-904b9bb8a0f7
* (Try to) use the conversion oracle also in w_unify to choose which constant toGravatar msozeau2008-10-03
| | | | | | | | | | | | unfold first. The patch changes the usual order of unifications so some may differ (only one example in the stdlib breaks because of more unification happening). Actually this change was trigerred because of an incompleteness which is not resolved here. At least this way unfolding is consistent between w_unify and the kernel. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11427 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing constr_cmp, propagating subtyping only right of a productGravatar puech2008-10-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11425 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correcting a delta normalization bug in VM (checked by benjamin)Gravatar jforest2008-09-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11423 85f007b7-540e-0410-9357-904b9bb8a0f7
* Partial fix for bug #1948: recompute order of dependencies betweenGravatar msozeau2008-09-25
| | | | | | | | | evars at the end of unification as later evars can refer to previous ones. This removes the assumption that evars are already ordered in eterm's code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11419 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #1943 and restrict the inference optimisation of Program toGravatar msozeau2008-09-15
| | | | | | | cases where coercion could not occur as well. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11414 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #1936: uncaught exception due to undefinable exceptions.Gravatar msozeau2008-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11405 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #1940: uncaught exception when searching for a type class.Gravatar msozeau2008-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11403 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix a bug, in fold_constr_with_binders, the types of fixpoints wereGravatar msozeau2008-09-13
| | | | | | | processed in the larger context instead of the bodies. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11400 85f007b7-540e-0410-9357-904b9bb8a0f7
* Better handling of the opacity of proof obligations, add the possibility ofGravatar msozeau2008-09-07
| | | | | | | overriding the default tactic when adding a definition. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11373 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix camlp5-ism "Ploc.Exc" and add a unification fix: when solving anGravatar msozeau2008-09-04
| | | | | | | | | | evar, do unification between the evar type and the type of the instance to properly propagate information. Typical example: in context ?A : Type, ?R : relation ?A. When we instantiate ?R using a goal like x = y by @eq t, we need to instantiate A to t as well. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11357 85f007b7-540e-0410-9357-904b9bb8a0f7
* Propagating commit 11343 from branch v8.2 to trunk (wish 1934 aboutGravatar herbelin2008-09-02
| | | | | | | | backtracking on coercion classes when a coercion path fails). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11344 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix implementation of "Global Instance" which redeclared the sameGravatar msozeau2008-08-27
| | | | | | | instance multiple times at each section closing (still a hack). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11338 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction de bugs:Gravatar herbelin2008-08-05
| | | | | | | | | | | | | - evarconv: mauvaise idée d'utiliser la conversion sur la tête d'un terme applicatif au moment de tester f u1 .. un = g v1 .. vn au premier ordre : on revient sur l'algo tel qu'il était avant le commit 11187. - Bug #1887 (format récursif cassé à cause de la vérification des idents). - Nouveau choix de formattage du message "Tactic Failure". - Nettoyage vocabulaire "match context" -> "match goal" au passage. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11305 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug de filtrage sous-terme #1920 introduit dans commitGravatar herbelin2008-08-05
| | | | | | | | | 11126 et qui faisait qu'on ne backtrackait en fait plus sur les sous-termes d'un terme qui lui filtrait. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11304 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite 11187 et 11298 : ne retarder le dépliage d'une projectionGravatar herbelin2008-08-05
| | | | | | | | | | | canonique que si elle contribue vraiment à une équation canonique, c'est-à-dire si son argument principal est une evar; sinon on répercute le comportement historique qui est de préférer le dépliage du côté droit d'une équation constante/constante. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11303 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 18:46:16 +0000