aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Collapse)AuthorAge
...
* Module type expressions of the form (Fsig X) with Definition foo := bar are ↵Gravatar soubiran2009-10-28
| | | | | | | | | | now accepted. +svn:ignore property on folders git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12429 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a new vernacular command for controling implicit generalization ofGravatar msozeau2009-10-27
| | | | | | | | | | | | | variables with syntax: [Local?|Global] Generalizable Variable(s)? [all|none|id1 idn]. By default no variable is generalizable, so this patch breaks backward compatibility with files that used implicit generalization (through Instance declarations for example). To get back the old behavior, one just needs to use [Global Generalizable Variables all]. Make coq_makefile more robust using [mkdir -p]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12428 85f007b7-540e-0410-9357-904b9bb8a0f7
* New cleaning phase of the Local/Global option managementGravatar herbelin2009-10-26
| | | | | | | | | - Clarification and documentation of the different styles of Local/Global modifiers in vernacexpr.ml - Addition of Global in sections for Open/Close Scope. - Addition of Local for Ltac when not in sections. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12418 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restore (and test) broken chaining of lemmas in "apply in" in presenceGravatar herbelin2009-10-25
| | | | | | | | | of side conditions. Fix a small presentation issue in printing the "exists" tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12416 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed bug in Czar grammarGravatar corbinea2009-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12415 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved the treatment of Local/Global options (noneffective Local onGravatar herbelin2009-10-25
| | | | | | | | | | | | Implicit Arguments, Arguments Scope and Coercion fixed, noneffective Global in sections for Hints and Notation detected). Misc. improvements (comments + interpretation of Hint Constructors + dev printer for hint_db). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12411 85f007b7-540e-0410-9357-904b9bb8a0f7
* This big commit addresses two problems:Gravatar soubiran2009-10-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 1- Management of the name-space in a modular development / sharing of non-logical objects. 2- Performance of atomic module operations (adding a module to the environment, subtyping ...). 1- There are 3 module constructions which derive equalities on fields from a module to another: Let P be a module path and foo a field of P Module M := P. Module M. Include P. ... End M. Declare Module K : S with Module M := P. In this 3 cases we don't want to be bothered by the duplication of names. Of course, M.foo delta reduce to P.foo but many non-logical features of coq do not work modulo conversion (they use eq_constr or constr_pat object). To engender a transparent name-space (ie using P.foo or M.foo is the same thing) we quotient the name-space by the equivalence relation on names induced by the 3 constructions above. To implement this, the types constant and mutual_inductive are now couples of kernel_names. The first projection correspond to the name used by the user and the second projection to the canonical name, for example the internal name of M.foo is (M.foo,P.foo). So: ************************************************************************************* * Use the eq_(con,mind,constructor,gr,egr...) function and not = on names values * ************************************************************************************* Map and Set indexed on names are ordered on user name for the kernel side and on canonical name outside. Thus we have sharing of notation, hints... for free (also for a posteriori declaration of them, ex: a notation on M.foo will be avaible on P.foo). If you want to use this, use the appropriate compare function defined in name.ml or libnames.ml. 2- No more time explosion (i hoppe) when using modules i have re-implemented atomic module operations so that they are all linear in the size of the module. We also have no more unique identifier (internal module names) for modules, it is now based on a section_path like mechanism => we have less substitutions to perform at require, module closing and subtyping but we pre-compute more information hence if we instanciate several functors then we have bigger vo. Last thing, the checker will not work well on vo(s) that contains one of the 3 constructions above, i will work on it soon... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12406 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a notation bug when extending binder_constr with empty levelsGravatar herbelin2009-10-17
| | | | | | | | | (see Notations.v). Improved the "already occurs in a different scope" test and message. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12399 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removal of trailing spaces.Gravatar serpyc2009-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12371 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add support for Local Declare ML ModuleGravatar glondu2009-09-29
| | | | | | | Instead of failing with some obscure error message *after* loading the module, accept Local Declare ML Module with the usual semantics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12366 85f007b7-540e-0410-9357-904b9bb8a0f7
* Complement to 12347 and 12348 on the extended syntax of case/elim.Gravatar herbelin2009-09-27
| | | | | | | | | | | | | | | Don't change the semantics of "case 1" and forbid the use of numbers to refer to non-dependent quantified hypotheses in the more general forms that are synonymous of "destruct" (don't want to commit to a syntax for non-dependent quantified hypotheses which is ambiguous and after all not so appealing: for instance, something like destruct @1, destruct #1, or destruct at 1, or destruct :(ind_pattern), meaning in the latter case the first hypothesis whose type matches ind_pattern, would have probably been better). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12355 85f007b7-540e-0410-9357-904b9bb8a0f7
* Only one "in" clause in "destruct" even for a multiple "destruct".Gravatar herbelin2009-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12348 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add "case as/in/using" and temporary "destruct" with n args.Gravatar herbelin2009-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12347 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
* - Addition of "Reserved Infix" continued.Gravatar herbelin2009-09-14
| | | | | | | | - Tried an extension of the lexer that supports keywords starting with a letter w/o being an ident (e.g. 'U+'). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12326 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Inductive types in the "using" option of auto/eauto/firstorder areGravatar herbelin2009-09-13
| | | | | | | | | | | | | | interpreted as using the collection of their constructors as hints. - Add support for both "using" and "with" in "firstorder". Made the syntax of "using" compatible with the one of "auto" by separating lemmas by commas. Did not fully merge the syntax: auto accepts constr while firstorder accepts names (but are constr really useful?). - Added "Reserved Infix" as a specific shortcut of the corresponding "Reserved Notation". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12325 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11
| | | | | | | | | | | | | | | string in most commands expecting a global name (e.g. 'Print "+"' for an infix notation or 'Print "{ _ } + { _ }"' for a misfix notation, possibly surrounded by a scope delimiter). Support for such smart globals in VERNAC EXTEND to do. Added a file smartlocate.ml for high-level globalization functions. Mini-nettoyage metasyntax.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added syntax "exists bindings, ..., bindings" for iterated "exists".Gravatar herbelin2009-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12316 85f007b7-540e-0410-9357-904b9bb8a0f7
* Postpone checking of Local/Global to allow grammar extensions to use itGravatar msozeau2009-09-02
| | | | | | | too. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12304 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de la gestion de Local et Global pour les options (au sens deGravatar aspiwack2009-08-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | Goptions). - Local Set/Unset ... change la valeur de l'option pour la section en cours (ou le module si il n'y a pas de section), l'option est restaurée à sa valeur précédente au sortir de la section. - Set/Unset ... survit aux sections mais pas aux modules. - Global Set/Unset ... survit aux sections et aux modules. Il y a une légère source d'incompatibilité là, Set avait le comportement de Local Set. Ça n'apparaît pas dans la lib standard, mais sait-on jamais. Les étapes suivantes : - Supprimer la notion d'option asynchrone, je n'en vois vraiment pas l'intérêt. Changer le type de retour de declare_option à unit aussi serait probablement une bonne idée. - Ajouter le support Local/Global à d'autres commandes sur le même modèle. Conflicts: parsing/g_vernac.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12280 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added profile.cmo in grammar.cma so that any functions in one of theGravatar herbelin2009-08-14
| | | | | | files embedded in grammar.cma can be profiled with the Profile module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12279 85f007b7-540e-0410-9357-904b9bb8a0f7
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
| | | | | | | | | | only used to allow a module to be ended before the summaries were restored what can be solved by moving upwards the place where the summaries are restored). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12275 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add support for "Infix ... := constr" instead of just "Infix ... := ref".Gravatar herbelin2009-08-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12269 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed incorrect optimization in Prettyp.pr_located_qualid introducedGravatar herbelin2009-08-07
| | | | | | | | | in commit r12265. Add a few synonyms back in Libnames/Nameops to maintain some minimal compatibility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12267 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
| | | | | | | | | | | | | | | (uniformisation of function names, classification). One of the most visible change is the renaming of section_path into full_path (the use of name section was obsolete due to the module system, but I don't know if the new name is the best chosen one - especially it remains some "sp" here and there). - Simplification of the interface of classify_object (first argument dropped). - Simplification of the code for vernac keyword "End". - Other small cleaning or dead code removal. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12265 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added "etransitivity".Gravatar herbelin2009-08-03
| | | | | | | | | | | | Added support for "injection" and "discriminate" on JMeq. Seized the opportunity to update coqlib.ml and to rely more on it for finding the equality lemmas. Fixed typos in coqcompat.ml. Propagated symmetry convert_concl fix to transitivity (see 11521). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12259 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
| | | | | | | | | | | | | | | - add coqtop option "-compat X.Y" so as to provide compatibility with previous versions of Coq (of course, this requires to take care of providing flags for controlling changes of behaviors!), - add support for option names made of an arbitrary length of words (instead of one, two or three words only), - add options for recovering 8.2 behavior for discriminate, tauto, evar unification ("Set Tactic Evars Pattern Unification", "Set Discriminate Introduction", "Set Intuition Iff Unfolding"). Update of .gitignore git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12258 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Granted wish #2138 (support for local binders in syntax of Record fields).Gravatar herbelin2009-07-15
| | | | | | | | - Add tests related to commits 12229 (bug #2117) and 12241 (bug #2139). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12242 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
* Allow anonymous instances again, with syntax [Instance: T] where TGravatar msozeau2009-06-15
| | | | | | | may be a product. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12188 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplifying the call to print_no_goals and not calling it when no goalGravatar herbelin2009-06-11
| | | | | | | | is ongoing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12184 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Added two new introduction patterns with the following temptative syntaxes:Gravatar herbelin2009-06-07
| | | | | | | | | | | | | | - "*" implements Arthur Charguéraud's "introv" - "**" works as "; intros" (see also "*" in ssreflect). - Simplifying the proof of Z_eq_dec, as suggested by Frédéric Blanqui. - Shy attempt to seize the opportunity to clean Zarith_dec but Coq's library is really going anarchically (see a summary of the various formulations of total order, dichotomy of order and decidability of equality and in stdlib-project.tex in branch V8revised-theories). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12171 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0Gravatar herbelin2009-06-06
| | | | | | | instead of the index required by the user; extended FixRule and Cofix accordingly). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12168 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ensure the precondition of the partial function [list_chop] holdsGravatar msozeau2009-06-03
| | | | | | | before calling it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12162 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un printer modulaire pour les constr. C'est-à-dire une fonctionGravatar aspiwack2009-05-28
| | | | | | | | | | | | qui permet de changer la façon dont on imprime certains sous-termes sans avoir à réécrire entièrement un printer de constr. Dans le même esprit que les commits sur le parser et le lexer, je cherche à donner une flexibilité aux plugins pour changer l'aspect de Coq pour le plier à d'autres conventions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12151 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une fonction Lexer.remove_keyword pour libérer un keyword dansGravatar aspiwack2009-05-27
| | | | | | | un plugin. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12147 85f007b7-540e-0410-9357-904b9bb8a0f7
* =?utf-8?q?D=C3=A9sinterdiction=20de=20GDELETE=5FRULE=20dans=20pcoq.ml4.=20Ma ↵Gravatar aspiwack2009-05-27
| | | | | | | | | | | | | | | | | lheureusement,=20je=20ne =20sais=20pas=20permettre=20que=20GDELETE=5FRULE=20soit=20appelable=20pendant=20une=20section =20sans=20causer=20de=20potentiels=20soucis=20(bien=20que=20je=20trouve=20qu'il=20faille=20un =20esprit=20sacr=C3=A9ment=20pervers=20pour=20faire=20Declare=20ML=20Module=20dans=20une=20section).?= MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit Je suppose qu'on est dans le même esprit d'information trop partielle que pour les notations aux niveaux 8, 99 et 200. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12146 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixing declarative mode in presence of high use of Change_evars nodesGravatar herbelin2009-05-20
| | | | | | | | | | | | | (bug 2092 and decl_mode.v in test suite). - Added a debugging printer for pftreestate. - Fixing American spelling in RefMan-decl.tex. - Optimizing application of tactic validation by removing consistency test in descend. - Fixing printing ambiguity for Hint Rewrite ->/<- in extratactics.ml4. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12134 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceGravatar herbelin2009-05-09
| | | | | | | | | | | | | as hints (see wish #2104). - New type hint_entry for interpreted hint. - Better centralization of functions dealing with evaluable_global_reference. - Unfortunately, camlp4 does not factorize rules so that "Hint Resolve" had uglily to be factorized by hand. - Typography in RefMan-tac.tex. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12121 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixed a little bug in previous commit (bad failure in case of unknown entry).Gravatar herbelin2009-04-27
| | | | | | | | - Added support for list of intropattern in Tactic Notation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12109 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Cleaning (unification of ML names, removal of obsolete code,Gravatar herbelin2009-04-27
| | | | | | | | | | | | | reorganization of code) and documentation (in pcoq.mli) of the code for parsing extensions (TACTIC/VERNAC/ARGUMENT EXTEND, Tactic Notation, Notation); merged the two copies of interp_entry_name to avoid they diverge. - Added support in Tactic Notation for ne_..._list_sep in general and for (ne_)ident_list(_sep) in particular. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12108 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixing #2090 (occur check missing when trying to solve evar-evar equation).Gravatar herbelin2009-04-25
| | | | | | | | | | - Adding test file related to commit 12080 (bug #2091). - Cleaning old parsing stuff from 8.0. - Support for camlp5 in base_include. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12106 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
| | | | | | | | | | | | | | This commit concerns about the first half of the useless code mentionned by Oug for coqtop (without plugins). For the moment, Oug is used in a mode where any elements mentionned in a .mli is considered to be precious. This already allows to detect and remove about 600 lines, and more is still to come. Among the interesting points, the type Entries.specification_entry and its constructors SPExxx were never used. Large parts of cases.ml (and hence subtac_cases.ml) were also useless. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12069 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixingGravatar herbelin2009-04-08
| | | | | | | | | | | Not_found bug in Theorem with) from V8.2 to trunk. - Improving indentation in presence of tabulation and utf-8 when reporting error messages with "^^^^^^". - Updating a few svn:ignore properties. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12059 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid inadvertent declaration of "on" as a keyword. New syntax isGravatar msozeau2009-03-29
| | | | | | | | {measure ms [id] [(rel)]}. Fix script of bug #2083 and test-suite file accordingly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12032 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
* 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
* Remove unused mli filesGravatar letouzey2009-03-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12023 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixed bug 2058 (as much as possible - the syntax of "pose (f binders := ...)"Gravatar herbelin2009-03-23
| | | | | | | | is not so robust). - Updating CHANGES git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12008 85f007b7-540e-0410-9357-904b9bb8a0f7
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20
| | | | | | | | | | | | | | | | | | | | | | | | * generalize the use of .mllib to build all cma, not only in plugins/ * the .mllib in plugins/ now mention Bruno's new _mod.ml files * lots of .cmo enumerations in Makefile.common are removed, since they are now in .mllib * the list of .cmo/.cmi can be retreive via a shell script line, see for instance rule install-library * Tolink.core_objs and Tolink.ide now contains ocaml _modules_, not _files_ * a -I option to coqdep_boot allows to control piority of includes (some files with the same names in kernel and checker ...) This is quite a lot of changes, you know who to blame / report to if something breaks. ... and last but not least I've started playing with ocamlbuild. The myocamlbuild.ml is far from complete now, but it already allows to build coqtop.{opt,byte} here. See comments at the top of myocamlbuild.ml, and don't hesitate to contribute, either for completing or simplifying it ! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12002 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 10:07:16 +0000