aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
Commit message (Collapse)AuthorAge
...
* 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
* Always add the Coq_config.dirs to xdg_dirsGravatar pboutill2012-05-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15265 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added an interface call to exit Coqtop nicely.Gravatar ppedrot2012-05-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15263 85f007b7-540e-0410-9357-904b9bb8a0f7
* Program: avoid staying in program mode after a failed Program commandGravatar letouzey2012-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15247 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding newline after warning and restoring distinction betweenGravatar herbelin2012-04-15
| | | | | | fatal and non fatal identifier check errors. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15178 85f007b7-540e-0410-9357-904b9bb8a0f7
* lib directory is cut in 2 cma.Gravatar pboutill2012-04-12
| | | | | | | | | | | | | | | - Clib that does not depend on camlpX and is made to be shared by all coq tools/scripts/... - Lib that is Coqtop specific As a side effect for the build system : - Coq_config is in Clib and does not appears in makefiles - only the BEST version of coqc and coqmktop is made - ocamlbuild build system fails latter but is still broken (ocamldebug finds automatically Unix but not Str. I've probably done something wrong here.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15144 85f007b7-540e-0410-9357-904b9bb8a0f7
* Shortcuts and optimizations of comparisonsGravatar xclerc2012-04-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15118 85f007b7-540e-0410-9357-904b9bb8a0f7
* info_trivial, info_auto, info_eauto, and debug (trivial|auto)Gravatar letouzey2012-03-30
| | | | | | | | | | | | | | | | | | | | | | | To mitigate the lack of a general "info" tactical, let's introduce some specialized tactics info_trivial, info_auto and info_eauto that display the basic tactics used when solving a goal. We also add tactics "debug trivial" and "debug auto" which display every basic tactics attempted by trivial or auto. Triggering the "info" or "debug" mode for auto, eauto, trivial can also be done now via global options, such as Set Debug Auto or Set Info Eauto. In case both debug and info modes are activated, the debug mode takes precedence. NB: it would be nice to name these tactics "info xxx" instead of "info_xxx", but I don't see how to implement a "info eauto" in eauto.ml4 (hence by TACTIC EXTEND) while keeping a generic "info foo" tactic in g_ltac.ml4 (useful to display a nice message about the unavailability of the general info). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15103 85f007b7-540e-0410-9357-904b9bb8a0f7
* Unification: Added a heuristic to solve problems of the formGravatar herbelin2012-03-26
| | | | | | | | | | | | | | | | | | ?x[t1..tm] = ?y[u1..un] when ?x occurs in u1..un with no (easy) way to know if it occurs in rigid position or not. Such equations typically come from matching problems such as "match a return ?T[a] with pair a1 a2 => a1 end" where, a is in type "?A * ?B", and, in the branch, the return clause, of the form "?T[pair ?A ?B a1 a2]", has to be unified with ?A. This possible dependency is kept since commits r15060-15062. The heuristic is to restrict ?T so that the dependency is removed, leading to a behavior similar to the one existing before these commits. This allows BGsection15.v, from contrib Ssreflect, to compile as it did before these commits. Also, removed one function exported without true need in r15061. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15092 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reorganizing the structure of evarutil.ml (only restructuration, noGravatar herbelin2012-03-20
| | | | | | change of semantics). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15060 85f007b7-540e-0410-9357-904b9bb8a0f7
* Yet another subtlety with bug 2732: when several grammar rules of aGravatar herbelin2012-03-18
| | | | | | | | | | | | | | | | | | TACTIC EXTEND block possibly parse the stand-alone name of a tactic, then only the first rule must be registered in the atomic tactic table so as to be consistent with what happens when the tactic is invoked directly via its parsing rules and not via the interpretation of a reference in the atomic tactic table. Concretely, this affects TACTIC EXTEND blocks of the form TACTIC EXTEND foo [ "bar" tactic_opt(tac) -> ... ] | [ "bar" constr_list(tac) -> ... ] where both rules parses "bar" alone but only the first rule must be registered in the atomic table, git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15046 85f007b7-540e-0410-9357-904b9bb8a0f7
* Second step of integration of Program:Gravatar msozeau2012-03-14
| | | | | | | | - Remove useless functorization of Pretyping - Move Program coercion/cases code inside pretyping/, enabled according to a flag. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15033 85f007b7-540e-0410-9357-904b9bb8a0f7
* Noise for nothingGravatar pboutill2012-03-02
| | | | | | | | | | | Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
* make mli-doc fixGravatar pboutill2012-01-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14905 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 15:52:57 +0000