aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init
Commit message (Collapse)AuthorAge
* No more use of tauto in Init/Gravatar pboutill2012-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14918 85f007b7-540e-0410-9357-904b9bb8a0f7
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14718 85f007b7-540e-0410-9357-904b9bb8a0f7
* SearchAbout and similar: add a customizable blacklistGravatar letouzey2011-08-11
| | | | | | | | | | | | | | | | | | | | | | | | Instead of hard-coding in search.ml some substrings such as "_admitted" or "_subproof" we don't want to see in results of SearchAbout and co, we now have a user command: Add Search Blacklist "foo". Remove Search Blacklist "foo". (* the opposite *) Print Table Search Blacklist. (* the current state *) In Prelude.v, three substrings are blacklisted originally: - "_admitted" for internal lemmas due to admit. - "_subproof" for internal lemmas due to abstract. - "Private_" for hiding auxiliary modules not meant for global usage. Note that substrings are searched in the fully qualified names of the available lemmas (e.g. "Coq.Init.Peano.plus"). This commit also adds the prefix "Private_" to some internal modules in Numbers, Z, N, etc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14408 85f007b7-540e-0410-9357-904b9bb8a0f7
* Take benefit of bullets available by default in PreludeGravatar herbelin2011-08-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14401 85f007b7-540e-0410-9357-904b9bb8a0f7
* Less ambitious application of a notation for eq_rect. We proposedGravatar herbelin2011-08-10
| | | | | | | | | | | | | | | | | | "rewrite Heq in H" but "rewrite" is sometimes used by users and I don't want to have to change their file. The solution to put the notations in a module does not work with name "rewrite" because loading the module would change the status of "rewrite" from simple ident to keyword (and we cannot declare "rewrite" as an ident, as shown in previous commit). Then we come back on notation "rew" (this name is also used by some users), in a module. This continues commit r14366 and r14390 and improves on the level of the notation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14400 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved the declaration of "Classic" being the default proof mode to coqtop.ml ↵Gravatar aspiwack2011-08-09
| | | | | | so that the files in Init can benefit from the full-blown tactic language. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14392 85f007b7-540e-0410-9357-904b9bb8a0f7
* New proposition "rewrite Heq in H" for eq_rect (assuming that there isGravatar herbelin2011-08-08
| | | | | | a smaller risk that "rewrite" clashes with a name used for constr). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14390 85f007b7-540e-0410-9357-904b9bb8a0f7
* All the parameters of or can be implicits.Gravatar pboutill2011-07-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14296 85f007b7-540e-0410-9357-904b9bb8a0f7
* Same Implicit Arguments rule for sumbool and sumor.Gravatar pboutill2011-07-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14295 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tentative abbreviation "rew Heq in H" for eq_rect. (feedback welcome)Gravatar herbelin2011-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14281 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a characterization of unique existence.Gravatar herbelin2011-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14277 85f007b7-540e-0410-9357-904b9bb8a0f7
* Arithemtic: more concerning compare, eqb, leb, ltbGravatar letouzey2011-06-20
| | | | | | | | | | | | | | | | | | | | Start of a uniform treatment of compare, eqb, leb, ltb: - We now ensure that they are provided by N,Z,BigZ,BigN,Nat and Pos - Some generic properties are derived in OrdersFacts.BoolOrderFacts In BinPos, more work about sub_mask with nice implications on compare (e.g. simplier proof of lt_trans). In BinNat/BinPos, for uniformity, compare_antisym is now (y ?= x) = CompOpp (x ?=y) instead of the symmetrical result. In BigN / BigZ, eq_bool is now eqb In BinIntDef, gtb and geb are kept for the moment, but a comment advise to rather use ltb and leb. Z.div now uses Z.ltb and Z.leb. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14227 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some simplifications in NZDomainGravatar letouzey2011-06-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14226 85f007b7-540e-0410-9357-904b9bb8a0f7
* Wf.iter_nat becomes Peano.nat_iter (with an implicit arg)Gravatar letouzey2011-05-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14103 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modularization of BinNat + fixes of stdlibGravatar letouzey2011-05-05
| | | | | | | | | | | | A sub-module N in BinNat now contains functions add (ex-Nplus), mul (ex-Nmult), ... and properties. In particular, this sub-module N directly instantiates NAxiomsSig and includes all derived properties NProp. Files Ndiv_def and co are now obsolete and kept only for compat git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14100 85f007b7-540e-0410-9357-904b9bb8a0f7
* Better comments and organisation in Datatypes.vGravatar letouzey2011-05-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14095 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing an "apply -> ... in hyp" bug (the hyp was considered as a fixedGravatar herbelin2011-04-28
| | | | | | ident by Ltac). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14074 85f007b7-540e-0410-9357-904b9bb8a0f7
* Init: some results in Type should rather be Defined than QedGravatar letouzey2011-03-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13920 85f007b7-540e-0410-9357-904b9bb8a0f7
* CompareSpec: a slight generalization/reformulation of CompSpecGravatar letouzey2011-03-17
| | | | | | | | | | | | | | | | | | | CompareSpec expects 3 propositions Peq Plt Pgt instead of 2 relations eq lt and 2 points x y. For the moment, we still always use (Peq=eq x y), (Plt=lt x y) (Pgt=lt y x), but this may not be always the case, especially for Pgt. The former CompSpec is now defined in term of CompareSpec. Compatibility is preserved (except maybe a rare unfold or red to break the CompSpec definition). Typically, CompareSpec looks nicer when we have infix notations, e.g. forall x y, CompareSpec (x=y) (x<y) (y<x) (x?=x) while CompSpec is shorter when we directly refer to predicates: forall x y, CompSpec eq lt x y (compare x y) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13914 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
| | | | | | | | | | | | | | | | According to B. Gregoire, this stuff is obsolete. Fine control on when to launch the VM in conversion problems is now provided by VMcast. We were already almost never boxing definitions anymore in stdlib files. "(Un)Boxed Definition foo" will now trigger a parsing error, same with Fixpoint. The option "(Un)Set Boxed Definitions" aren't there anymore, but tolerated (as no-ops), since unknown options raise a warning instead of an error by default. Some more cleaning could be done in the vm. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13806 85f007b7-540e-0410-9357-904b9bb8a0f7
* First release of Vector library.Gravatar pboutill2010-12-10
| | | | | | | | | | To avoid names&notations clashs with list, Vector shouldn't be "Import"ed but one can "Import Vector.VectorNotations." to have notations. SetoidVector at least remains to do. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13702 85f007b7-540e-0410-9357-904b9bb8a0f7
* Used multiple lists of implicit arguments to transfer the choices ofGravatar herbelin2010-10-23
| | | | | | | | | | Program in terms of implicit arguments to the rest of the library. This commit only covers the case of list of implicit arguments that have a different length in Program (e.g. inl, Vcons) but not the case of implicit arguments which differs only in their maximality status (e.g. pair). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13575 85f007b7-540e-0410-9357-904b9bb8a0f7
* Using multiple lists of implicit arguments in Program for preservingGravatar herbelin2010-10-03
| | | | | | | | | | | | | | the compatibility with the rest of the theories. Used multiple lists of implicit arguments in Init only when the maximality status is not modified in Program (and thus the compatibility is strictly preserved). This improves the compatibility for the implicit arguments of eq_refl and JMeq_refl between 8.2 and 8.3 when using Program (up to the residual differences in the maximality status). For the constants Acc_inv, inl, inr, left, right, Vnil, Vcons, the compatibility with 8.2 is not improved but the consistency between Program and the rest of the library is. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13485 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made notations for exists, exists! and notations of Utf8.v recursive notationsGravatar herbelin2010-07-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13317 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bool: shorter and more systematic proofs + an iff lemma about eqbGravatar letouzey2010-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13286 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bool: iff lemmas about or, a reflect inductive, an is_true functionGravatar letouzey2010-07-10
| | | | | | | | | | | For the moment, almost no lemmas about (reflect P b), just the proofs that it is equivalent with an P<->b=true. is_true b is (b=true), and is meant to be added as a coercion if one wants it. In the StdLib, this coercion is not globally activated, but particular files are free to use Local Coercion... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13275 85f007b7-540e-0410-9357-904b9bb8a0f7
* clear/revert dependent: restrict to hyp(h) instead of ident(h)Gravatar letouzey2010-06-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13169 85f007b7-540e-0410-9357-904b9bb8a0f7
* New tactic "clear dependent", for the moment in ltac in Init/TacticsGravatar letouzey2010-06-17
| | | | | | | | | | | for the moment, only one hypothesis name is accepted after clear dependent (seems to be also the case for generalize dependent). Btw, added an alternative name "revert dependent" for "generalize dependent", since this tactics remove hypothesis from the context. To be documentated later... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13161 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a fairly large commit (around 140 files and 7000 lines of code impacted), it will cause some troubles for sure (I've listed the know regressions below, there is bound to be more). At this state of developpement it brings few features to the user, as the old tactics were ported with no change. Changes are on the side of the developer mostly. Here comes a list of the major changes. I will stay brief, but the code is hopefully well documented so that it is reasonably easy to infer the details from it. Feature developer-side: * Primitives for a "real" refine tactic (generating a goal for each evar). * Abstract type of tactics, goals and proofs * Tactics can act on several goals (formally all the focused goals). An interesting consequence of this is that the tactical (. ; [ . | ... ]) can be separated in two tacticals (. ; .) and ( [ . | ... ] ) (although there is a conflict for this particular syntax). We can also imagine a tactic to reorder the goals. * Possibility for a tactic to pass a value to following tactics (a typical example is an intro function which tells the following tactics which name it introduced). * backtracking primitives for tactics (it is now possible to implement a tactical '+' with (a+b);c equivalent to (a;c+b;c) (itself equivalent to (a;c||b;c)). This is a valuable tool to implement tactics like "auto" without nowing of the implementation of tactics. * A notion of proof modes, which allows to dynamically change the parser for tactics. It is controlled at user level with the keywords Set Default Proof Mode (this is the proof mode which is loaded at the start of each proof) and Proof Mode (switches the proof mode of the current proof) to control them. * A new primitive Evd.fold_undefined which operates like an Evd.fold, except it only goes through the evars whose body is Evar_empty. This is a common operation throughout the code, some of the fold-and-test-if-empty occurences have been replaced by fold_undefined. For now, it is only implemented as a fold-and-test, but we expect to have some optimisations coming some day, as there can be a lot of evars in an evar_map with this new implementation (I've observed a couple of thousands), whereas there are rarely more than a dozen undefined ones. Folding being a linear operation, this might result in a significant speed-up. * The declarative mode has been moved into the plugins. This is made possible by the proof mode feature. I tried to document it so that it can serve as a tutorial for a tactic mode plugin. Features user-side: * Unfocus does not go back to the root of the proof if several Focus-s have been performed. It only goes back to the point where it was last focused. * experimental (non-documented) support of keywords BeginSubproof/EndSubproof: BeginSubproof focuses on first goal, one can unfocus only with EndSubproof, and only if the proof is completed for that goal. * experimental (non-documented) support for bullets ('+', '-' and '*') they act as hierarchical BeginSubproof/EndSubproof: First time one uses '+' (for instance) it focuses on first goal, when the subproof is completed, one can use '+' again which unfocuses and focuses on next first goal. Meanwhile, one cas use '*' (for instance) to focus more deeply. Known regressions: * The xml plugin had some functions related to proof trees. As the structure of proof changed significantly, they do not work anymore. * I do not know how to implement info or show script in this new engine. Actually I don't even know what they were suppose to actually mean in earlier versions either. I wager they would require some calm thinking before going back to work. * Declarative mode not entirely working (in particular proofs by induction need to be restored). * A bug in the inversion tactic (observed in some contributions) * A bug in Program (observed in some contributions) * Minor change in the 'old' type of tactics causing some contributions to fail. * Compilation time takes about 10-15% longer for unknown reasons (I suspect it might be linked to the fact that I don't perform any reduction at QED-s, and also to some linear operations on evar_map-s (see Evd.fold_undefined above)). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12961 85f007b7-540e-0410-9357-904b9bb8a0f7
* Arith's min and max placed in Peano (+basic specs max_l and co)Gravatar letouzey2010-02-17
| | | | | | | This allow for instance to remove the dependency of List.v toward Min.v To prove max_l and co, we push Le.le_pred and Le.le_S_n into Peano. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12784 85f007b7-540e-0410-9357-904b9bb8a0f7
* CompSpec2Type is used to build functions, it should be Defined, not QedGravatar letouzey2010-02-13
| | | | | | This solves in particular the compilation failure of contrib ATBR git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12765 85f007b7-540e-0410-9357-904b9bb8a0f7
* CompSpecType, a clone of CompSpec but in Type instead of PropGravatar letouzey2010-02-12
| | | | | | | | | | | In interfaces fields like compare_spec, a CompSpec is prefered to get nice extraction, but then no "destruct (compare_spec .. ..)" is possible in a Type context. Now you can say there "destruct (CompSpec2Type (compare_spec ... ...))" This translate to the Type variant, and make the analysis on it (which is equivalent to analysing the comparison directly). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12753 85f007b7-540e-0410-9357-904b9bb8a0f7
* Init/Logic: commutativity and associativity of /\ and \/Gravatar letouzey2010-01-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12643 85f007b7-540e-0410-9357-904b9bb8a0f7
* Factorisation between Makefile and ocamlbuild systems : .vo to compile are ↵Gravatar letouzey2009-12-09
| | | | | | | | | | | | in */*/vo.itarget On the way: no more -fsets (yes|no) and -reals (yes|no) option of configure if you want a partial build, make a specific rule such as theories-light Beware: these vo.itarget should not contain comments. Even if this is legal for ocamlbuild, the $(shell cat ...) we do in Makefile can't accept that. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12574 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some lemmas about dependent choice + extensions of Compare_dec +Gravatar herbelin2009-11-16
| | | | | | synonyms in Le.v, Lt.v, Gt.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12527 85f007b7-540e-0410-9357-904b9bb8a0f7
* Datatypes.length and app defined back via fun+fix instead of FixpointGravatar letouzey2009-11-06
| | | | | | | | Since length and app were defined inside a Section in List.v, their type argument A wasn't inside the fixpoint. Restoring the initial definition repairs (at least) Cachan/IntMap. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12477 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
* 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
* Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'Gravatar letouzey2009-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12380 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
* 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
* New tactic to rewrite decidability lemmas when one knows which sideGravatar herbelin2009-08-24
| | | | | | | | | | | | is true. E.g. "decide (eq_nat_dec n 0) with H" on H: n=0 |- (if eq_nat_dec n 0 then 1 else 2) = 1 returns H: n=0 |- 1 = 1 . git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12291 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed extra space in printing notation { x & P } + minor other thingsGravatar herbelin2009-08-11
| | | | | | (shorter proof of O_S in trunk + typo). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12271 85f007b7-540e-0410-9357-904b9bb8a0f7
* OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArithGravatar letouzey2009-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12250 85f007b7-540e-0410-9357-904b9bb8a0f7
* Miscellaneous practical commits: Gravatar herbelin2009-06-29
| | | | | | | | | | | | - theories: made a hint database with the constructor of eq_true - coqide: binding F5 to About dans coqide + made coqide aware of string interpretation inside comments - lexer: added warning when ending comments inside a strings itself in a comment - xlate: completed patten-matching on IntroForthComing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12217 85f007b7-540e-0410-9357-904b9bb8a0f7
* Parsing files for numerals (+ ascii/string) moved into pluginsGravatar letouzey2009-03-27
| | | | | | | | | | | | | | Idea: make coqtop more independant of the standard library. In the future, we can imagine loading the syntax for numerals right after their definition. For the moment, it is easier to stay lazy and load the syntax plugins slightly before the definitions. After this commit, the main (sole ?) references to theories/ from the core ml files are in Coqlib (but many parts of coqlib are only used by plugins), and it mainly concerns Init (+ Logic/JMeq and maybe a few others). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12024 85f007b7-540e-0410-9357-904b9bb8a0f7
* Better mechanism for loading initial pluginsGravatar letouzey2009-03-14
| | | | | | | | | | | | | | | | Instead of dirty hacks in toplevel/coqtop.ml, we simply add some Declare ML Module in Prelude.v. Gain: now that coqdep is clever enough, dependencies are automatic, and we can simplify the Makefile quite a lot: no more references to INITPLUGINSBEST and the like. Besides, mltop.ml4 can also be simplified a lot: by giving $(CONTRIBSTATIC) to coqmktop instead of contrib.cma, now coqtop is aware that it already contain the static plugins (or not), and subsequent ML Module are ignored correctly without us having to do anything :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11979 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 04:14:44 +0000