aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
Commit message (Collapse)AuthorAge
...
* 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
* 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
* 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
* 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
* 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
* 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
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bigint: new functions of_int and to_int, 2nd arg of pow in intGravatar letouzey2012-08-02
| | | | | | | | | | | | * Many of_string and to_string could be replaced by of_int and to_int when the number isn't too large. NB: to_int may raise a Failure if the number is larger than max_int. * In numbers_syntax, computing the height of bigN trees via bigint is *really* overkill, int should be enough there : this limits printable/parsable bigN to (2^31)^(2^max_int) ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15669 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bigint: adds a missing -1 in hugo's last commit 15659Gravatar letouzey2012-07-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15666 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bigint : better ensure canonicity of arrays of int blocksGravatar letouzey2012-07-30
| | | | | | | | | | | | | | | | | | | | | In the chosen representation of negative numbers, (-base) is actually legal as first element of an int array. This situation was wrongly handled by many functions in this module, leading to possible non-canonical representation of a big number, and hence faulty "equal" answers or buggy output of "to_string". For instance, on a 32-bit machine : open Big_int;; to_string (sub (of_string "-10000") (of_string "-1000000"));; (* was displaying 9810000 instead of 990000 *) Also simplified "of_string", which now rely on "neg" for handling negative numbers. Btw, improved checks comparing w.r.t OCaml's Big_int instead of float. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15665 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bigint: avoid dependency over PpGravatar letouzey2012-07-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15664 85f007b7-540e-0410-9357-904b9bb8a0f7
* Better fixing propagation of carry in sub_mult used for euclidianGravatar herbelin2012-07-29
| | | | | | | division over unbounded integers (thanks again to L. Théry for pointing out the remaining problem in r15637). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15659 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing unchecked overflow in sub_mult used for euclidian division overGravatar herbelin2012-07-21
| | | | | | unbounded integers (thanks to L. Théry for pointing out the problem). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15637 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reductionops refactoringGravatar pboutill2012-07-20
| | | | | | | | | | | Semantic changes are : - whd_nored_stack remplaces a defined meta by its value whereas the old whd_stack didn't. - Zcase and Zfix are alwais put on stack. iota_flag is checked by constructors and cofix. - simpl uses its own whd_ function that do not touch at matched term git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15634 85f007b7-540e-0410-9357-904b9bb8a0f7
* Put Option in ClibGravatar pboutill2012-07-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15631 85f007b7-540e-0410-9357-904b9bb8a0f7
* A new status Unsafe in Interface. Meant for commands such as Admitted.Gravatar aspiwack2012-07-12
| | | | | | | | | | | Currently : - only Admitted uses the Unsafe return status - the status is ignored in coqtop - Coqide sees the status but apparently doesn't use it for colouring (I'm not sure why, but then again, it's not as if I understood coqide's code or anything) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15610 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adapting the IDE interface with the focussed display.Gravatar ppedrot2012-07-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15579 85f007b7-540e-0410-9357-904b9bb8a0f7
* Notation: a new annotation "compat 8.x" extending "only parsing"Gravatar letouzey2012-07-05
| | | | | | | | | | | | | | | | | | | | | | Suppose we declare : Notation foo := bar (compat "8.3"). Then each time foo is used in a script : - By default nothing particular happens (for the moment) - But we could get a warning explaining that "foo is bar since coq > 8.3". For that, either use the command-line option -verb-compat-notations or the interactive command "Set Verbose Compat Notations". - There is also a strict mode, where foo is forbidden : the previous warning is now an error. For that, either use the command-line option -no-compat-notations or the interactive command "Unset Compat Notations". When Coq is launched in compatibility mode (via -compat 8.x), using a notation tagged "8.x" will never trigger a warning or error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15514 85f007b7-540e-0410-9357-904b9bb8a0f7
* Now CoqIDE separates answer and messages. This should hopefullyGravatar ppedrot2012-06-29
| | | | | | be backward compatible... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15501 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing info_auto / info_trivial display.Gravatar ppedrot2012-06-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15497 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed string width printing in string_of_ppcmdsGravatar ppedrot2012-06-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15493 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a Deque module to CLib (to be used in CoqIDE).Gravatar ppedrot2012-06-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15492 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation of pp.mliGravatar ppedrot2012-06-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15487 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving logging level to Interface.Gravatar ppedrot2012-06-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15486 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing Camlp4 compilation (hopefully, preprocessing fixpoint reached...)Gravatar ppedrot2012-06-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15482 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
| | | | | | | | | | were closed (i.e. the only remaining ones are those of printing/parsing). Meanwhile, a simplified interface is provided in loc.mli. This also permits to put Pp in Clib, because it does not depend on CAMLP4/5 anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing #2825.Gravatar ppedrot2012-06-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15469 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2809 (anomaly when printing a module with notations due toGravatar herbelin2012-06-20
| | | | | | | bad interaction between lazy evaluation of pp streams and temporary effectful extension of global environment). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15457 85f007b7-540e-0410-9357-904b9bb8a0f7
* Partialy revert "coq_makefile fixup" because old Makefiles still need CAMLP4BINGravatar pboutill2012-06-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15441 85f007b7-540e-0410-9357-904b9bb8a0f7
* coq_makefile fixupGravatar pboutill2012-06-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15438 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug 2805: Only export CAMLP4LIB if camlp4 -where ends successfullyGravatar pboutill2012-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15434 85f007b7-540e-0410-9357-904b9bb8a0f7
* Colorization of coqtop messages is turned *off* by defaultGravatar letouzey2012-06-07
| | | | | | | | | | | | | This bling-bling feature is interacting badly with - the documentation generation - the bench logs - compilation in an emacs buffer - ... As long as these points aren't solved, no coloring by default, but on the contrary an option to manually activate it: coqtop -color git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15427 85f007b7-540e-0410-9357-904b9bb8a0f7
* A box to pretty-print them all.Gravatar ppedrot2012-06-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15424 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a color output to Coqtop.Gravatar ppedrot2012-06-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15421 85f007b7-540e-0410-9357-904b9bb8a0f7
* Separated notice vs info messages, and cleaned up the interface a bit.Gravatar ppedrot2012-06-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15420 85f007b7-540e-0410-9357-904b9bb8a0f7
* Flushing formatters before program exit.Gravatar ppedrot2012-06-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15415 85f007b7-540e-0410-9357-904b9bb8a0f7
* More cleaningGravatar ppedrot2012-06-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15414 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning Pp.ppnl useGravatar ppedrot2012-06-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15413 85f007b7-540e-0410-9357-904b9bb8a0f7
* Getting rid of Pp.msgnl and Pp.message.Gravatar ppedrot2012-06-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15412 85f007b7-540e-0410-9357-904b9bb8a0f7
* Getting rid of Pp.msgGravatar ppedrot2012-05-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15400 85f007b7-540e-0410-9357-904b9bb8a0f7
* More uniformisation in Pp.warn functions.Gravatar ppedrot2012-05-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15399 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vernacexpr is now a mli-only file, locality stuff now in locality.mlGravatar letouzey2012-05-29
| | | | | | Adds a directory ./intf for pure interfaces. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15367 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert copy/pasted function in to minilib thanks to clib.cmaGravatar pboutill2012-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15352 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added semantic completion in CoqIDE. (Should also add an option for that...)Gravatar ppedrot2012-05-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15317 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a SearchAbout-like primitive in coqtop interface.Gravatar ppedrot2012-05-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15313 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added an interface primitive to ask coqtop for its internal versions.Gravatar ppedrot2012-05-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15312 85f007b7-540e-0410-9357-904b9bb8a0f7
* Slightly modified the coqtop interface by adding an identifier inGravatar ppedrot2012-05-11
| | | | | | goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15303 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 05:02:56 +0000