aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2012-09-15Some documentation and cleaning of CList and Util interfaces.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15805 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14Added some tricky tail-rec versions of List functions to CListppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15803 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14Partial revert of Yann commit in order to use CLib.List when openingppedrot
Util module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15802 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
List module. That way, an "open Util" in the header permits using any function of CList in the List namespace (and in particular, this permits optimized reimplementations of the List functions, as, for example, tail-rec implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
compiler warnings). I was afraid that such a brutal refactoring breaks some obscure invariant about linking order and side-effects but the standard library still compiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15800 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14lib/Pp:regisgia
Backtrack on the removal of a type definition. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15799 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14kernel/Term:regisgia
Backtrack on a type definition that was moved by error by the previous patch. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15798 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
especially about unused definitions, unused opens and unused rec flags. The following patch uses information gathered using these warnings to clean Coq source tree. In this patch, I focused on warnings whose fix are very unlikely to introduce bugs. (a) "unused rec flags". They cannot change the semantics of the program but only allow the inliner to do a better job. (b) "unused type definitions". I only removed type definitions that were given to functors that do not require them. Some type definitions were used as documentation to obtain better error messages, but were not ascribed to any definition. I superficially mentioned them in one arbitrary chosen definition to remove the warning. This is unaesthetic but I did not find a better way. (c) "unused for loop index". The following idiom of imperative programming is used at several places: "for i = 1 to n do that_side_effect () done". I replaced "i" with "_i" to remove the warning... but, there is a combinator named "Util.repeat" that would only cost us a function call while improving readibility. Should'nt we use it? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15797 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-13Made Pp.std_ppcmds opaque.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15795 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-12Coqide uses Glib to get the XDG_DATA/CONFIG_HOME/DIRSpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15793 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-10Moved Pp to CLib. In particular, Pp does not depend on CAMLP4/5ppedrot
anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15792 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-10Fixed #2893.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15790 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-10Added Print Assumptions command to CoqIDEppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15788 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-09When asked for a SearchAbout request, Coq now returns a more preciseppedrot
name, that is, a pair of a smart qualified name and the missing prefix needed to recover the full path. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15787 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-09Fixed bug #2895ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15785 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-07Makefile: revised install-coqide ruleletouzey
Thanks Russel O'Connor for spotting this remaining use of $(COQIDEOPT) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15784 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-07Avoid [Loading ML file ...] messages when launching coqtopletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15783 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-07Coqdoc: fix --utf8 bug for pretty printingpboutill
Author: Francois Ripault <francois.ripault@epita.fr> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15782 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-06Added a comment/uncomment command to CoqIDEppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15781 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-06Fix computation of obligations for mutually recursive definitions.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15780 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-06Nice output of SearchAbout command in CoqIDEppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15779 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-05Obsolete syntax in documentation of Solve Obligation commands.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15778 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-05Rationalized the behaviour of "Next Obligation" and "Admit Obligations"ppedrot
commands. When several programs are being defined, the argumentless version of these commands does not complain anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15777 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-05A few fixes in configure file:herbelin
- Fixing parsing of option -custom - More precise documentation of which option expects an argument - Deprecation of obviously obsolete -emacs option git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15773 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-04Fix coqide compilation with lablgtk 2.16pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15772 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-04Coqide Fix highlighting of Extraction, Import, Variablespboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15771 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-04test-suite: fix grep rule for output testspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15770 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-04test-suite uses coqtop instead of coqtop.bytepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15769 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-04Erase %.vo dependency to the phony target statespboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15768 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-24In the output tests, ignore dynlink messagesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15767 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-24correct some ends of .mllib files (avoid a broken tolink.ml)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15766 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-24Use fully-qualified Coq.Init.Prelude when starting coqtopletouzey
This avoids interferences with another Prelude.v around (cf. Orsay/Random) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15765 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-24Fix Extraction Implicit on axioms.aspiwack
There was a small bug causing the type in OCaml commentary not to honor the implicit declaration, whereas the rest of the code did. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15764 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-24Experimental support for a comment in the files' preamble in extraction.aspiwack
Scheme comments are output on a single line because Ocaml's Format module which serves as a backend to Pp has an integer, rather than a string as identation value, so we cannot make it so that each new line in the comment starts with ";; ". I've tried something with Pp.ifb but it was hackish at best and had somewhat strange results. Known bug: as Pp.std_ppcmds is non-persistent, the comment is actually printed only once per Extraction command, even if it outputs several files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15763 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-24Add option Set/Unset Extraction Conservative Types.aspiwack
Extracted code need not preserve typing relations (e:t) from the source code. This may be a problem as the extracted code may not implement the intented interface. This option disables the optimisations which would prevent an extracted term's type to be its extracted source term's type. At this point the only such optimization is (I think) removing some dummy λ-abstractions in constant definitions. Extraction Implicit is still honored in this mode, and it's mostly necessary to produce reasonable types. So in the conservative type mode, which abstractions can be removed and which can'tt is entirely under the user's control. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15762 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-24Better highlighting of strings in coqide.aspiwack
Strings were not highlighted out of comments. This would lead to funny result, like certain strings (i.e. "(*") to cause all following code to be highlighted as a string. I've added strings in three different contexts (the same where comments are highlighted). I think it's safe to do, I don't know if it's the best way, though. In particular I don't know if it's the best way to highlight notations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15761 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-24Assumption commands are now displayed as unsafe in Coqide.aspiwack
They are still marked as safe if they are part of a module type, though. Also local assumptions such as "Hypothesis" or "Context" are displayed as unsafe if they happen to be defined without a section. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15760 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-24Modification of the unjustified tag.aspiwack
It seemed to intrusive to have it display the text underlined and red. The goal of this tag is to notify the user when Coq doesn't guarantee correctness, not to make the command look like an error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15759 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-24Correcting a comment in pattern-matching compilation.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15758 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23test-suite: Local Tactic Notation is now legal since r15731letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15757 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23CHANGES: document the end of states/initial.coq and coqtop.optletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15756 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23Remove a script unused since 2006 (cf commit r8626)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15755 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23myocamlbuild : fixes for new printing directory + sourceview for coqideletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15754 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23No more states/initial.coq, instead coqtop now requires Prelude.voletouzey
For starting a bare coqtop, the recommended option is now "-noinit" that skips the load of Prelude.vo. Option "-nois" is kept for compatibility, it is now an alias to "-noinit". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15753 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23No more coqtop.opt, produce directly a coqtop binaryletouzey
We now always produce two binaries, coqtop and coqtop.byte : - If ocamlopt is available, coqtop is directly what used to be coqtop.opt, no more symlinks needed. - Otherwise, coqtop is a copy of coqtop.byte. The same for coqchk and coqide... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15752 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23No need anymore to refer to COQLIB in ocamldebug-coqletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15751 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23Revert "when cross-compiling with mingw32, let's fix the Filename.dir_sep"letouzey
This was merely cosmetic after all, since recent Windows versions do tolerate paths with /. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15750 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23Configure + Makefile : simplification when -localletouzey
When local=true: - "make install" is now a no-op - In configure, no need hence to fill the various variables about installation (BINDIR, COQLIBINSTALL, MANDIR, DOCDIR, EMACSLIB). This avoids many references to absolute location of the coq sources (which may contain blanks or other strange chars in win32). - For the moment, we keep CONFIGDIR and DATADIR, used when launching coqide from inside the build directory. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15749 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23configure: get rid of the -src option and of ${COQSRC}letouzey
The -src option was antic and probably broken (many references to source files without the $COQRSC prefix). Instead, it's quite simpler to refer to paths in relative way (and safer in win32 where the base path may include spaces and other horrors). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15748 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 06:14:43 +0000