aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2009-03-27GroebnerZ: no more admitted lemmasletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12022 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-26Ocamlbuild: 1st reasonably complete version (rules for binaries + plugins + vo)letouzey
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
2009-03-26Fixes in Program well-founded definitions:msozeau
- 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
2009-03-26ocamlbuild: coqide, coqchk, a bit of .voletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12019 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-26Coqdep_boot: one line with bad indentationletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12018 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-26Protect typeset arguments in titles in LaTeX output (fixes compilationmsozeau
errors in Library.coqdoc). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12017 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-26clean revision and coqdep_boot, toolmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12016 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-26bin/coq-{parser,interface}: use this coqtop, not the first in $PATHlmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12015 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-25make coqdep_boot in stage1, not stage2lmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12014 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-24Fix coqdoc bugs reported by Ian Lynagh.msozeau
- 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
2009-03-24ocamlbuild improvements + minor makefile fixletouzey
* 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
2009-03-24pretty.mll of coqdoc becomes cpretty.mll (avoid clash with a camlp5 file)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12011 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-23- Fixed bug 2058 (as much as possible - the syntax of "pose (f binders := ...)"herbelin
is not so robust). - Updating CHANGES git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12008 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-22Backport from v8.2 branch of 11986 (interpretation of quantifiedherbelin
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
2009-03-22Compromise wrt introduction-names compatibility issue after additionherbelin
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
2009-03-22More elaborate handling of newlines in Gallina mode. Support inlinemsozeau
Qed's. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12005 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-22coqdoc fixes and support for parsing regular comments (request bymsozeau
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
2009-03-20Many changes in the Makefile infrastructure + a beginning of ocamlbuildletouzey
* 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
2009-03-20Makefile: avoid $(ML4FILES:.ml4=.ml) since this is $(ML4FILESML)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12001 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-20replaced dir_load by load_file because dir_load does not raise an exception ↵barras
when loading fails git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12000 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-20delete contrib dirsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11999 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-20Fixes to make Ynot compile with the trunk:msozeau
- 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
2009-03-20Compatibility with Apple's non-gnu sed.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11997 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵letouzey
user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-19coq_makefile: -c and -shared conflict; tacinterp: delay evaluation of tactic ↵barras
genargs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11995 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-18renamed %-mod.ml into %_mod.ml to avoid ocaml warningbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11994 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-18fixed ring/field warning about hyp cleaning upbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11993 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-18removed correctness dirsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11992 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-18coq_makefile: no ml dependency on coq sourcesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11991 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-17Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11990 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-17- gros commit sur ring et field: passage des arguments simplifiebarras
- 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
2009-03-17Makefile:clean: rm *-mod.mlbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11988 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-17- configure: affiche si le natdynlink est positionnebarras
- 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
2009-03-16missing -c option of ocamlc in coq_makefile; coqdep_boot main loop was ↵barras
included in coqdep git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11985 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-16coqdep_boot: a specialized and dependency-free coqdep for killing one of the ↵letouzey
build stages git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11984 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-16Makefile: fix ignored errors, several attempts to clarify thingsletouzey
* 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
2009-03-16Makefile: minor improvementsletouzey
* 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
2009-03-16Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"herbelin
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
2009-03-14Cleaning/uniformizing the interface of tacticals.mliherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11980 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-14Better mechanism for loading initial pluginsletouzey
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
2009-03-14RefMan: a label defined twiceletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11978 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-14Makefile: ml dependencies of contribs are moved to .mllib filesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11977 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-14Coqdep: better handling of Declare ML Module (via .mllib) + many cleanupsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11976 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-14Coqdep: remove references to obsolete .zi and Require Implementation stuffletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11975 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-11Cleanup: avoid the warning about Coq-tex not being a valid Ocaml module nameletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11974 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-11Cleanup: remove unused config/giveostype.mlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11973 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-11Cleanup: remove 3 unused files in ide/letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11972 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-11Cleanup: remove old correctness files, unused for a long timeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11971 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-09in natdynlink, lack of uniformity between general %.vo and Init/%.vo rules ↵barras
resulted in cyclic dependencies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11970 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-09Optionally list opaque constants in addition to axions/variables inmsozeau
assumptions. Feel free to rename "Print Opaque Dependencies" to something better. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11969 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-23 17:51:59 +0000