aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Program
Commit message (Collapse)AuthorAge
...
* Fix premature optimisation in dependent induction: even variable args needGravatar msozeau2009-04-10
| | | | | | | | | | | to be generalized as they may appear in other arguments or their types. Try to keep the original names around as well, using the ones found in the goal. This only requires that interning a pattern [forall x, _] properly declares [x] as a metavariable, binding instances are already part of the substitutions computed by [extended_matches]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12079 85f007b7-540e-0410-9357-904b9bb8a0f7
* Experimental support for automatic destruction of recursive calls andGravatar msozeau2009-04-08
| | | | | | | | | clearing of recursive protototypes in Program obligations. Relies on marking said prototypes with a particular constant and preprocessing obligation goals with an appropriate tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12071 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
| | | | | | | | | | | | | | | - The measure can now refer to all the formal arguments - The recursive calls can make all the arguments vary as well - Generalized to any relation and measure (new syntax {measure m on R}) This relies on an automatic curryfication transformation, the real fixpoint combinator is working on a sigma type of the arguments. Reduces to the previous impl in case only one argument is involved. The patch also introduces a new flag on implicit arguments that says if the argument has to be infered (default) or can be turned into a subgoal/obligation. Comes with a test-suite file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12030 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
* - Better deal with commands inside section titles in latex output usingGravatar msozeau2009-01-21
| | | | | | | | the support from hyperref. - Rename n-ary 'exist' tactic to 'exists' in Program.Syntax. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11821 85f007b7-540e-0410-9357-904b9bb8a0f7
* Move FunctionalExtensionality to Logic/ (someone please check that theGravatar msozeau2008-12-16
| | | | | | | | | | doc is ok). Rework the .v files in Program accordingly, adding some documentation and proper headers. Integrate the development of an elimination principle for measured functions in Program/Wf by Eelis van der Weegen. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11686 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
* Generalized binding syntax overhaul: only two new binders: `() and `{},Gravatar msozeau2008-12-14
| | | | | | | | | | | | | | | | | guessing the binding name by default and making all generalized variables implicit. At the same time, continue refactoring of Record/Class/Inductive etc.., getting rid of [VernacRecord] definitively. The AST is not completely satisfying, but leaning towards Record/Class as restrictions of inductive (Arnaud, anyone ?). Now, [Class] declaration bodies are either of the form [meth : type] or [{ meth : type ; ... }], distinguishing singleton "definitional" classes and inductive classes based on records. The constructor syntax is accepted ([meth1 : type1 | meth1 : type2]) but raises an error immediately, as support for defining a class by a general inductive type is not there yet (this is a bugfix!). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11679 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix a bug in the specialization by unification tactic related to the problemsGravatar msozeau2008-11-07
| | | | | | | | given by injection. Add the example to the test-suite for [dependent destruction]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11551 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix for bug #1973 provided by Brian Campbell.Gravatar msozeau2008-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11492 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite 11472 et 11473Gravatar herbelin2008-10-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11474 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various little improvements:Gravatar msozeau2008-09-25
| | | | | | | | | | | | | | - A new [dependent pattern] tactic to do a pattern on an object in an inductive family and generalize by both the indexes and the object itself. Useful to prepare a goal for elimination with a dependent principle. - Better dependent elimination simplification tactic that doesn't throw away non-dependent equalities if they can't be injected. - Add [fold_sub] and [unfold_sub] tactics for folding/unfolding well-founded definitions using measures built by Program. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11420 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report improvements in Equations to the dependent elimination tactic:Gravatar msozeau2008-09-15
| | | | | | | | | | | - Do not touch at the user equalities and so on by using a blocking constant. This avoids the wild autoinjections and subst tactics that were used before. Thanks to Brian Aydemir for an example were this hurt a lot. - Debug the tactic used to simplify induction hypotheses. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11415 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finish debugging the unification machinery in [Equations]. Do the _compGravatar msozeau2008-09-13
| | | | | | | | | | dance when defining a new program by default, which forces use of JMeq but makes for much more robust tactics. Everything in success/Equations works except for limitations due to JMeq or the guardness checker (one example seems to actually diverge...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11402 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove redefinition of id in Program.Basics, just add maximal implicits.Gravatar msozeau2008-09-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11401 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a type argument to letin_tac instead of using casts and recomputingGravatar msozeau2008-09-12
| | | | | | | | | when one wants a particular type. Rewrite of the unification behind [Equations], much more robust but still buggy w.r.t. inaccessible patterns. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11399 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add enough information to correctly globalize recursive calls in inductive andGravatar msozeau2008-09-11
| | | | | | | | | recursive definitions and references to previous fields in record and classes definitions. Fixes the corresponding typesetting issue in coqdoc output. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11397 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix a bug reintroduced in [setoid_reflexivity] etc...Gravatar msozeau2008-09-09
| | | | | | | | Go back to refine_hyp instead of specialize, because only the former handles open terms. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11391 85f007b7-540e-0410-9357-904b9bb8a0f7
* More debugging of [Equations], now able to discharge even the heavilyGravatar msozeau2008-09-07
| | | | | | | | dependent [noConfusion] definitions in "A Few Constructions on Constructors". Now the guardness check is blocking. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11374 85f007b7-540e-0410-9357-904b9bb8a0f7
* Better handling of recursive Equations definitions... still not perfect.Gravatar msozeau2008-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11356 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correct handling of implicit arguments in [Equations] definitions,Gravatar msozeau2008-09-03
| | | | | | | | support for "where" notation declarations as well. Better checking of recursivity or not, after type-checking. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11354 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add support for recursive definitions to [Equations], deciding if aGravatar msozeau2008-09-02
| | | | | | | | definition is recursive or not based on occurence of a rec call in the body. Examples updated, enjoy! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11353 85f007b7-540e-0410-9357-904b9bb8a0f7
* Initial implementation of a new command to define (dependent) functions byGravatar msozeau2008-09-02
| | | | | | | | | | | | | | | | | | | | | | equations. It is essentially an implementation of the "Eliminating Dependent Pattern-Matching" paper by Goguen, McBride and McKinna, relying on the new dependent eliminations tactics. The bulk is in contrib/subtac/equations.ml4. It implements a tree splitting on a set of clauses and the generation of a corresponding proof term along with some obligations at each splitting node. The obligations are solved by driving the dependent elimination tactic and you get a complete proof term at the end with the code given by the equations at the right spots, the rest of the cases being pruned automatically. Does not support recursion yet, a file with examples is in the test-suite. With recursion, it would be similar to Agda 2's pattern matching, except it won't reduce in Coq due to JMeq's/K. Incidentally, the simplification tactics after dependent elimination have been improved, resulting in a clearer and more space efficient implementation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11352 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes in dependent induction tactic to keep names, allow givingGravatar msozeau2008-08-21
| | | | | | | | intro-patterns and avoid useless generalizations on inductive parameters. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11331 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes in generalize_eqs/dependent induction to allow the user to specifyGravatar msozeau2008-07-28
| | | | | | | generalized variables himself. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11280 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add test-suite file for bug# 1905 and minor fix in Program/Equality.Gravatar msozeau2008-07-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11245 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
| | | | | | | | | | majuscule - si pas un ident ou un terme - et se terminent par un point). Restent quelques utilisations de "error" qui sont liées à des usages internes, ne faudrait-il pas utiliser des exceptions plus spécifiques à la place ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11230 85f007b7-540e-0410-9357-904b9bb8a0f7
* Autour du parsing:Gravatar herbelin2008-07-15
| | | | | | | | | | | | | | | | | | - Utilisation de notations de type "abbreviation paramétrée" plutôt que de notations introduisant des mots-clés, là où c'est possible (cela affecte QDen, in_left/in_right, inhabited, S/P dans NZCyclic). - Extension du lexeur pour qu'il prenne le plus long token valide au lieu d'échouer sur un plus long préfixe non valide de token (permet notamment de faire passer la notation de Georges "'C_ G ( A )" sans invalider toute séquence commençant par 'C et non suivie de _) - Rajout d'un point final à certains messages d'erreur qui n'en avaient pas. - Ajout String.copy dans string_of_label ("trou" de mutabilité signalé par Georges -- le "trou" lié aux vecteurs des noeuds App restant lui ouvert). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11225 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rename obligations_tactic to obligation_tactic and fix bugs #1893.Gravatar msozeau2008-06-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11164 85f007b7-540e-0410-9357-904b9bb8a0f7
* Temporary fix for bug #1876, printing fails because of unresolvedGravatar msozeau2008-06-13
| | | | | | | globals. Change program_simpl to use [auto] and not [auto with *]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11124 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
* Fix setoid_rewrite documentation examples.Gravatar msozeau2008-06-03
| | | | | | | | | | Debug handling of identifiers in coqdoc (should work with modules and sections) and add missing macros. Move theories/Program to THEORIESVO to put the files in the standard library documentation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11046 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improve the dependent induction tactic to automatically find theGravatar msozeau2008-05-30
| | | | | | | | generalized hypotheses. Also move part of the tactic to ML and improve the generated proof term in case of non-dependent induction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11023 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various fixes:Gravatar msozeau2008-05-15
| | | | | | | | | | | | - Fix a typo in lowercase_utf8 - Fix generation of signatures in subtac_cases not working for dependent inductive types with dependent indices. - Fix coercion of inductive types generating ill-typed terms. - Fix test script using new syntax for Instances. - Move simpl_existTs to Program.Equality and use it in simpl_depind. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10932 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used toGravatar msozeau2008-05-12
| | | | | | | | | | | | | | | | | | | change the default pretty-printing to use Π, λ instead of forall and fun (and allow "," as well as "=>" for "fun" to be more consistent with the standard forall and exists syntax). Parsing allows theses new forms too, even if not in -unicode, and does not make Π or λ keywords. As usual, criticism and suggestions are welcome :) Not sure what to do about "->"/"→" ? - [setoid_replace by] now uses tactic3() to get the right parsing level for tactics. - Type class [Instance] names are now mandatory. - Document [rewrite at/by] and fix parsing of occs to support their combination. - Backtrack on [Enriching] modifier, now used exclusively in the implementation of implicit arguments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10921 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Cleanup parsing of binders, reducing to a single production for allGravatar msozeau2008-05-11
| | | | | | | | | | | | | | binders. - Change syntax of type class instances to better match the usual syntax of lemmas/definitions with name first, then arguments ":" instance. Update theories/Classes accordingly. - Correct globalization of tactic references when doing Ltac :=/::=, update documentation. - Remove the not so useful "(x &)" and "{{x}}" syntaxes from Program.Utils, and subset_scope as well. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10919 85f007b7-540e-0410-9357-904b9bb8a0f7
* Work on the "occurrences" tactic argument. It is now possible to passGravatar msozeau2008-04-20
| | | | | | | | | | lists of occurrences through tactics. Implement the "at" variants of setoid_replace correspondingly. Fix in class_tactics efor w_unify not checking types when unifying a meta with anything (problematic at top-level only). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10820 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
* Minor fixes: Gravatar msozeau2008-04-05
| | | | | | | | | - Allow unicode superscripts characters. - Put Program notations in scopes. - Correct priority semantics in typeclasses eauto. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10759 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes. Use expanded type in class_tactics for Morphism search, toGravatar msozeau2008-04-02
| | | | | | | | | | | alleviate some problems with delta. Better precedence in lambda notation. Temporarily deactivate notations for relation conjunction, equivalence and so on, while we search for a better syntax and maybe a generalization (fixes bug #1820). Better destruct_call in Program.Tactics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10742 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
| | | | | | | | pas correctes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10739 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improve error handling and messages for typeclasses. Gravatar msozeau2008-03-28
| | | | | | | | | | | | | | | | | Add definitions of relational algebra in Classes/RelationClasses including equivalence, inclusion, conjunction and disjunction. Add PartialOrder class and show that we have a partial order on relations. Change SubRelation to subrelation for consistency with the standard library. The caracterization of PartialOrder is a bit original: we require an equivalence and a preorder so that the equivalence relation is equivalent to the conjunction of the order relation and its inverse. We can derive antisymmetry and appropriate morphism instances from this. Also add a fully general heterogeneous definition of respectful from which we can build the non-dependent respectful combinator. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10728 85f007b7-540e-0410-9357-904b9bb8a0f7
* Interpret patterns for hypotheses types in match goal in type_scope (if not aGravatar msozeau2008-03-25
| | | | | | | | context [] pattern). May break some user contribs... Rename clsubstitute to substitute. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10716 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a flag to control rewriting under lambdas. Otherwise makes someGravatar msozeau2008-03-20
| | | | | | | | | | | | rewrite calls fail because an occurence is found under a lambda that was not found before and there are no adequate morphism declarations to make the rewrite succeed nor the possibility to give occurences to rewrite (yet). Only setoid_rewrite will try rewriting under lambda's for now. Example problem found in a port of the Random library. Also improved the required_library error message. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10704 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed unneeded tactics from RelationClasses. UseGravatar msozeau2008-03-16
| | | | | | | | check_required_library where needed (fixes bug #1797). Remove spurious messages from ring when not in verbose mode. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10685 85f007b7-540e-0410-9357-904b9bb8a0f7
* Misc: Add test for bug 1704, now closed. Add usual syntax for lists inGravatar msozeau2008-03-16
| | | | | | | | Program.Syntax along with stronger implicits. Update dependent induction test file using unicode syntax. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10682 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reorganize Program and Classes theories. Requiring Setoid no longer setsGravatar msozeau2008-03-16
| | | | | | | | | | | | implicits for left, inl or eq, hence some theories had to be changed again. It should make some user contribs compile again too. Also do not import functional extensionality when importing Program.Basics, add a Combinators file for proofs requiring it and a Syntax file for the implicit settings. Move Classes.Relations to Classes.RelationClasses to avoid name clash warnings as advised by Hugo and Pierre. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10681 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do a second pass on the treatment of user-given implicit arguments. NowGravatar msozeau2008-03-15
| | | | | | | | | | | | | | | | | | works in inductive type definitions and fixpoints. The semantics of an implicit inductive parameter is maybe a bit weird: it is implicit in the inductive definition of constructors and the contructor types but not in the inductive type itself (ie. to model the fact that one rarely wants A in vector A n to be implicit but in vnil yes). Example in test-suite/ Also, correct the handling of the implicit arguments across sections. Every definition which had no explicitely given implicit arguments was treated as if we asked to do global automatic implicit arguments on section closing. Hence some arguments were given implicit status for no apparent reason. Also correct and test the parsing rule which disambiguates between {wf ..} and {A ..}. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10677 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bugs that were reopened due to the change of setoidGravatar msozeau2008-03-08
| | | | | | | | | | | | | | | | | | implementation. Mostly syntax changes when declaring parametric relations, but also some declarations were relying on "default" relations on some carrier. Added a new DefaultRelation type class that allows to do that, falling back to the last declared Equivalence relation by default. This will be bound to Add Relation in the next commit. Also, move the "left" and "right" notations in Program.Utils to "in_left" and "in_right" to avoid clashes with existing scripts. Minor change to record to allow choosing the name of the argument for the record in projections to avoid possible incompatibilities. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10639 85f007b7-540e-0410-9357-904b9bb8a0f7
* Syntax changes in typeclasses, remove "?" for usual implicit argumentsGravatar msozeau2008-03-06
| | | | | | | | | | | | | | | | | | | | | binding, add "!" syntax for the new binders which require parameters and not superclasses. Change backquotes for curly braces for user-given implicit arguments, following tradition. This requires a hack a la lpar-id-coloneq. Change ident to global for typeclass names in class binders. Also requires a similar hack to distinguish between [ C t1 tn ] and [ c : C t1 tn ]. Update affected theories. While hacking the parsing of { wf }, factorized the two versions of fix annotation parsing that were present in g_constr and g_vernac. Add the possibility of the user optionaly giving the priority for resolve and exact hints (used by type classes). Syntax not fixed yet: a natural after the list of lemmas in "Hint Resolve" syntax, a natural after a "|" after the instance constraint in Instance declarations (ex in Morphisms.v). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10628 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 08:14:53 +0000