aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Complementary fix to have ocamlopt_shared_os5fix.sh working correctlyGravatar herbelin2009-03-31
| | | | | | | (tested on MacOS 10.5). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12042 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix the fix script for ocamlopt -shared in MacOS 10.5 (remarks by Hugo)Gravatar letouzey2009-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12041 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update CHANGESGravatar glondu2009-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12040 85f007b7-540e-0410-9357-904b9bb8a0f7
* Document new quote constructionGravatar glondu2009-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12039 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add tests for quoteGravatar glondu2009-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12038 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a more general quote constructionGravatar glondu2009-03-30
| | | | | | | | | | | | | | | | | "quote f [...] in c using t" will call t (must be an ltac function) with a X (of form "f x" or "f vm x") such that X converts to c. In particular, match goal with | H : ?x |- _ => quote f in x using (fun X => change X in H) end may be used as an equivalent of plain quote that acts on an hypothesis. The construction can be used in a more general way, though. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12037 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix some typos and spacesGravatar glondu2009-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12036 85f007b7-540e-0410-9357-904b9bb8a0f7
* Csdpcert: adaptation after last commitGravatar letouzey2009-03-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12035 85f007b7-540e-0410-9357-904b9bb8a0f7
* Micromega: improvement of the code obtained by extractionGravatar letouzey2009-03-29
| | | | | | | | | | | | | | | | | * In eval_cone and simpl_cone, default patterns were leading to duplicated computations. Adaptation of RingMicromega.v to prevent that. * Use the Ocaml builtin types (lists, pairs, bool, etc) and remove the useless conversion functions in mutils.ml and alii. * andb was extracted to a correctly lazy but ugly match. Let's rather use Ocaml's (&&). Remain to be done: take advantage of extraction during the build, - either directly if we are using plugins, (no dependency issues) - or if we compile statically, at least check later that the micromega.ml in the archive and the one auto-generated are in sync. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12034 85f007b7-540e-0410-9357-904b9bb8a0f7
* ocamlbuild: many improvements (macos 10.5 fix, correct dllpath, etc)Gravatar letouzey2009-03-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12033 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
* Fix useless redeclaration of a tactic name when UpdateTac is replayed.Gravatar msozeau2009-03-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12031 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
* Fix bug #2056 (discharge bug).Gravatar msozeau2009-03-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12029 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix static compilation of numeral syntax (typo in _mod files, sorry ...)Gravatar letouzey2009-03-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12028 85f007b7-540e-0410-9357-904b9bb8a0f7
* ZArith/Int: no need to load romega here (but rather in FullAVL)Gravatar letouzey2009-03-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12027 85f007b7-540e-0410-9357-904b9bb8a0f7
* ZMicromega: useless dependency toward ZArith.IntGravatar letouzey2009-03-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12026 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqdep: some dead code and code move (first experiment with Oug)Gravatar letouzey2009-03-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12025 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
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 02:10:48 +0000