aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Some documentation and cleaning of CList and Util interfaces.Gravatar ppedrot2012-09-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15805 85f007b7-540e-0410-9357-904b9bb8a0f7
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added some tricky tail-rec versions of List functions to CListGravatar ppedrot2012-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15803 85f007b7-540e-0410-9357-904b9bb8a0f7
* Partial revert of Yann commit in order to use CLib.List when openingGravatar ppedrot2012-09-14
| | | | | | Util module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15802 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
| | | | | | | | | 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
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
| | | | | | | | | | 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
* lib/Pp:Gravatar regisgia2012-09-14
| | | | | | 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
* kernel/Term:Gravatar regisgia2012-09-14
| | | | | | | 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
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Made Pp.std_ppcmds opaque.Gravatar ppedrot2012-09-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15795 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide uses Glib to get the XDG_DATA/CONFIG_HOME/DIRSGravatar pboutill2012-09-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15793 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved Pp to CLib. In particular, Pp does not depend on CAMLP4/5Gravatar ppedrot2012-09-10
| | | | | | anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15792 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed #2893.Gravatar ppedrot2012-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15790 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added Print Assumptions command to CoqIDEGravatar ppedrot2012-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15788 85f007b7-540e-0410-9357-904b9bb8a0f7
* When asked for a SearchAbout request, Coq now returns a more preciseGravatar ppedrot2012-09-09
| | | | | | | 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
* Fixed bug #2895Gravatar ppedrot2012-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15785 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: revised install-coqide ruleGravatar letouzey2012-09-07
| | | | | | 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
* Avoid [Loading ML file ...] messages when launching coqtopGravatar letouzey2012-09-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15783 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqdoc: fix --utf8 bug for pretty printingGravatar pboutill2012-09-07
| | | | | | 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
* Added a comment/uncomment command to CoqIDEGravatar ppedrot2012-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15781 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix computation of obligations for mutually recursive definitions.Gravatar msozeau2012-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15780 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nice output of SearchAbout command in CoqIDEGravatar ppedrot2012-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15779 85f007b7-540e-0410-9357-904b9bb8a0f7
* Obsolete syntax in documentation of Solve Obligation commands.Gravatar ppedrot2012-09-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15778 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rationalized the behaviour of "Next Obligation" and "Admit Obligations"Gravatar ppedrot2012-09-05
| | | | | | | 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
* A few fixes in configure file:Gravatar herbelin2012-09-05
| | | | | | | | - 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
* Fix coqide compilation with lablgtk 2.16Gravatar pboutill2012-09-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15772 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide Fix highlighting of Extraction, Import, VariablesGravatar pboutill2012-09-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15771 85f007b7-540e-0410-9357-904b9bb8a0f7
* test-suite: fix grep rule for output testsGravatar pboutill2012-09-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15770 85f007b7-540e-0410-9357-904b9bb8a0f7
* test-suite uses coqtop instead of coqtop.byteGravatar pboutill2012-09-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15769 85f007b7-540e-0410-9357-904b9bb8a0f7
* Erase %.vo dependency to the phony target statesGravatar pboutill2012-09-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15768 85f007b7-540e-0410-9357-904b9bb8a0f7
* In the output tests, ignore dynlink messagesGravatar letouzey2012-08-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15767 85f007b7-540e-0410-9357-904b9bb8a0f7
* correct some ends of .mllib files (avoid a broken tolink.ml)Gravatar letouzey2012-08-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15766 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use fully-qualified Coq.Init.Prelude when starting coqtopGravatar letouzey2012-08-24
| | | | | | | 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
* Fix Extraction Implicit on axioms.Gravatar aspiwack2012-08-24
| | | | | | | 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
* Experimental support for a comment in the files' preamble in extraction.Gravatar aspiwack2012-08-24
| | | | | | | | | | | | | | | 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
* Add option Set/Unset Extraction Conservative Types.Gravatar aspiwack2012-08-24
| | | | | | | | | | | | | | | | | 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
* Better highlighting of strings in coqide.Gravatar aspiwack2012-08-24
| | | | | | | | | | | | 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
* Assumption commands are now displayed as unsafe in Coqide.Gravatar aspiwack2012-08-24
| | | | | | | | 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
* Modification of the unjustified tag.Gravatar aspiwack2012-08-24
| | | | | | | | 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
* Correcting a comment in pattern-matching compilation.Gravatar aspiwack2012-08-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15758 85f007b7-540e-0410-9357-904b9bb8a0f7
* test-suite: Local Tactic Notation is now legal since r15731Gravatar letouzey2012-08-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15757 85f007b7-540e-0410-9357-904b9bb8a0f7
* CHANGES: document the end of states/initial.coq and coqtop.optGravatar letouzey2012-08-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15756 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove a script unused since 2006 (cf commit r8626)Gravatar letouzey2012-08-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15755 85f007b7-540e-0410-9357-904b9bb8a0f7
* myocamlbuild : fixes for new printing directory + sourceview for coqideGravatar letouzey2012-08-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15754 85f007b7-540e-0410-9357-904b9bb8a0f7
* No more states/initial.coq, instead coqtop now requires Prelude.voGravatar letouzey2012-08-23
| | | | | | | | 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
* No more coqtop.opt, produce directly a coqtop binaryGravatar letouzey2012-08-23
| | | | | | | | | | | 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
* No need anymore to refer to COQLIB in ocamldebug-coqGravatar letouzey2012-08-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15751 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert "when cross-compiling with mingw32, let's fix the Filename.dir_sep"Gravatar letouzey2012-08-23
| | | | | | | 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
* Configure + Makefile : simplification when -localGravatar letouzey2012-08-23
| | | | | | | | | | | | | | | 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
* configure: get rid of the -src option and of ${COQSRC}Gravatar letouzey2012-08-23
| | | | | | | | | 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.39.1) at 2024-08-02 05:25:15 +0000