aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* 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
* GroebnerZ: no more admitted lemmasGravatar letouzey2009-03-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12022 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ocamlbuild: 1st reasonably complete version (rules for binaries + plugins + vo)Gravatar letouzey2009-03-26
| | | | | | | | | | | | | | | | | | | | Dealing with .vo files was harder than anticipated (issues with coqdep_boot and the location of the .v files). Current solution cannot compete for a beauty prize, but well. Several other issues remain (see top and bottom of myocamlbuild.ml) - For the moment the coqlib / coqsrc in Coq_config is to be hacked by hand to add _build/ in it. - Parallelism is a "no go" for the moment. Ocamlbuild accepts a -j option, but it has almost no effect experimentally. (but at least it doesn't take more time than make -j1, i.e. about 14 min here, instead of about 7 for make -j2) - After a first full build, ocamlbuild is awfully slow to detect that nothing has to be redone (1 min 25 here) To be continued... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12021 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes in Program well-founded definitions:Gravatar msozeau2009-03-26
| | | | | | | | - de Bruijn bug #2083 - Avoid useless eta-expansion (bug #2060) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12020 85f007b7-540e-0410-9357-904b9bb8a0f7
* ocamlbuild: coqide, coqchk, a bit of .voGravatar letouzey2009-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12019 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqdep_boot: one line with bad indentationGravatar letouzey2009-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12018 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protect typeset arguments in titles in LaTeX output (fixes compilationGravatar msozeau2009-03-26
| | | | | | | errors in Library.coqdoc). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12017 85f007b7-540e-0410-9357-904b9bb8a0f7
* clean revision and coqdep_boot, tooGravatar lmamane2009-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12016 85f007b7-540e-0410-9357-904b9bb8a0f7
* bin/coq-{parser,interface}: use this coqtop, not the first in $PATHGravatar lmamane2009-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12015 85f007b7-540e-0410-9357-904b9bb8a0f7
* make coqdep_boot in stage1, not stage2Gravatar lmamane2009-03-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12014 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix coqdoc bugs reported by Ian Lynagh.Gravatar msozeau2009-03-24
| | | | | | | | - Add coqdoccomment LaTeX environment to sty file - Fix buggy parsing in comments git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12013 85f007b7-540e-0410-9357-904b9bb8a0f7
* ocamlbuild improvements + minor makefile fixGravatar letouzey2009-03-24
| | | | | | | | | | | * a small shell script ./build to drive ocamlbuild * rules for all the binaries (apart from coqide and coqchk) * use of ocamlbuild's Echo instead of using shell + sed + awk for generated files * Makefile: remove unused STAGE1_CMO and add bin/coqdep_boot to the list of things to "clean" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12012 85f007b7-540e-0410-9357-904b9bb8a0f7
* pretty.mll of coqdoc becomes cpretty.mll (avoid clash with a camlp5 file)Gravatar letouzey2009-03-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12011 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
* Backport from v8.2 branch of 11986 (interpretation of quantifiedGravatar herbelin2009-03-22
| | | | | | | | | | | hypotheses in induction, unbalanced parenthesis in ltac call stack printer) and 12003 (late update of CREDITS) + update of magic numbers (using a somehow arbitrary value between the 8.2 magic numbers and the possibly forthcoming 8.3 magic numbers). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12007 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compromise wrt introduction-names compatibility issue after additionGravatar herbelin2009-03-22
| | | | | | | | | | | | | | | | of new support for dependent "destruct" over terms in dependent types (r11944): dependencies in evars are not considered to be a cause of dependent "destruct". This solves one of the incompatibilities revealed in contribs. The other one comes from a "destruct_call" on a truly dependent goal. Fortunately, dependent destruct makes that destruct_call now works better and the corresponding script can be shortened (FSetAVL_prog). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12006 85f007b7-540e-0410-9357-904b9bb8a0f7
* More elaborate handling of newlines in Gallina mode. Support inlineGravatar msozeau2009-03-22
| | | | | | | Qed's. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12005 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqdoc fixes and support for parsing regular comments (request byGravatar msozeau2009-03-22
| | | | | | | | | | | | B. Pierce on coq-club). - Output regular comments, enclosed in a span in HTML (with (* *) delimiters) and inside a new environment in LaTeX. - HTML output: put the span inside anchors in links, so as to keep the same style as for definitions (customizable in the CSS). - Better handling of Next Obligation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12004 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
* Makefile: avoid $(ML4FILES:.ml4=.ml) since this is $(ML4FILESML)Gravatar letouzey2009-03-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12001 85f007b7-540e-0410-9357-904b9bb8a0f7
* replaced dir_load by load_file because dir_load does not raise an exception ↵Gravatar barras2009-03-20
| | | | | | when loading fails git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12000 85f007b7-540e-0410-9357-904b9bb8a0f7
* delete contrib dirsGravatar barras2009-03-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11999 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes to make Ynot compile with the trunk:Gravatar msozeau2009-03-20
| | | | | | | | | | | | | | | | - Choose one of the possible instances of an evar when considering remaining unification constraints: otherwise we just do nothing and some evars remain uninstantiated. - Normalise the goal w.r.t. evars before subst, to avoid a double vision problem: the substituted variable appears only in an instance of an evar and when we try the rewrite it has been substituted making the dependency disappear. - Hack to correcly handle let-in annotations which are internalized as casts: they're really typing constraints. Shouldn't we just change the AST to have the type at rawconstr let-in nodes? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11998 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibility with Apple's non-gnu sed.Gravatar msozeau2009-03-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11997 85f007b7-540e-0410-9357-904b9bb8a0f7
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵Gravatar letouzey2009-03-20
| | | | | | user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
* coq_makefile: -c and -shared conflict; tacinterp: delay evaluation of tactic ↵Gravatar barras2009-03-19
| | | | | | genargs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11995 85f007b7-540e-0410-9357-904b9bb8a0f7
* renamed %-mod.ml into %_mod.ml to avoid ocaml warningGravatar barras2009-03-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11994 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed ring/field warning about hyp cleaning upGravatar barras2009-03-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11993 85f007b7-540e-0410-9357-904b9bb8a0f7
* removed correctness dirsGravatar barras2009-03-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11992 85f007b7-540e-0410-9357-904b9bb8a0f7
* coq_makefile: no ml dependency on coq sourcesGravatar barras2009-03-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11991 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl)Gravatar herbelin2009-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11990 85f007b7-540e-0410-9357-904b9bb8a0f7
* - gros commit sur ring et field: passage des arguments simplifieGravatar barras2009-03-17
| | | | | | | | | | | - tacinterp.ml: les arguments tactiques de Tactic Notation n'etaient pas evalues, laissant des variables libres (symptome: exc Not_found) - reals: Open Local --> Local Open - ListTactics: syntaxe des listes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11989 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile:clean: rm *-mod.mlGravatar barras2009-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11988 85f007b7-540e-0410-9357-904b9bb8a0f7
* - configure: affiche si le natdynlink est positionneGravatar barras2009-03-17
| | | | | | | | | | | - coq_makefile: utilise Coq_config pour avoir la liste des contribs - mltop: normalisation des noms de modules ML (majuscule) - Makefiles: introduction de fichiers %-mod.ml qui se chargent de faire les declarations de modules ML d'un plugin git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11987 85f007b7-540e-0410-9357-904b9bb8a0f7
* missing -c option of ocamlc in coq_makefile; coqdep_boot main loop was ↵Gravatar barras2009-03-16
| | | | | | included in coqdep git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11985 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqdep_boot: a specialized and dependency-free coqdep for killing one of the ↵Gravatar letouzey2009-03-16
| | | | | | build stages git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11984 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: fix ignored errors, several attempts to clarify thingsGravatar letouzey2009-03-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | * I encountered error messages during compilation, for instance ocamlopt complaining about non-existing coq_config.cmi when compiling coq_config.ml. Moreover, make was _not_ stopping at these errors (WTF?!). After some debug, it turned out to be (indirectly) my fault: I placed earlier the inclusion of the new .mllib.d in Makefile.stage1, but this is too early, coqdep, which is used to compute these files, isn't built yet. Due to the semantics of "-include", make tries to build it, fails with the above error, and goes on happily. Arrgh. After moving the inclusion of these .mllib.d to Makefile.stage2, everything seems to work ok now. * Since we're using such "nice" non-trivial features of make, I've started a small FAQ section about them at the beginning of Makefile * Recursive calls to make are now done with two options: --no-builtin-rules : let's avoid builtin rules like "%:%.o" ... --warn-undefined-variable : using a non-defined variable isn't necessarily bad, but I found a few bugs with this option, and I suggest we keep it. * Clarified the rules about stage* in Makefile and their STAGE*_TARGETS variables in Makefile.common. Now a newcomer _might_ have a chance to grasp in less than a day what's going on ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11983 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: minor improvementsGravatar letouzey2009-03-16
| | | | | | | | * no need anymore for special rules for -rectypes: we use it everywhere * $(REVISIONCMO) is obsolete * avoid triple references to almost all files of kernel/ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11982 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"Gravatar herbelin2009-03-16
| | | | | | | | | | | | | | now works correctly, "unfold foo at 4 in H at 3" now fails correctly, etc.). The terminology for clauses (though I don't find the term "clause" very intuitive after all) is mostly preserved except for "simple_clause" which becomes a light form of "clause" instead of being an atom of clause (what played the role of "simple_clause" is now called "goal_location" - better names are welcome). Main changes are in tacticals.ml and tactics.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11981 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning/uniformizing the interface of tacticals.mliGravatar herbelin2009-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11980 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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
* RefMan: a label defined twiceGravatar letouzey2009-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11978 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: ml dependencies of contribs are moved to .mllib filesGravatar letouzey2009-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11977 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqdep: better handling of Declare ML Module (via .mllib) + many cleanupsGravatar letouzey2009-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11976 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqdep: remove references to obsolete .zi and Require Implementation stuffGravatar letouzey2009-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11975 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleanup: avoid the warning about Coq-tex not being a valid Ocaml module nameGravatar letouzey2009-03-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11974 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleanup: remove unused config/giveostype.mlGravatar letouzey2009-03-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11973 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleanup: remove 3 unused files in ide/Gravatar letouzey2009-03-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleanup: remove old correctness files, unused for a long timeGravatar letouzey2009-03-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11971 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 06:59:36 +0000