aboutsummaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Collapse)Author
2012-06-26Fixed string width printing in string_of_ppcmdsppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15493 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-26Added a Deque module to CLib (to be used in CoqIDE).ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15492 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-23Documentation of pp.mlippedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15487 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-23Moving logging level to Interface.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15486 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-22Fixing Camlp4 compilation (hopefully, preprocessing fixpoint reached...)ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15482 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
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
2012-06-21Fixing #2825.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15469 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-20Fixing bug #2809 (anomaly when printing a module with notations due toherbelin
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
2012-06-15Partialy revert "coq_makefile fixup" because old Makefiles still need CAMLP4BINpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15441 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-14coq_makefile fixuppboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15438 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-12bug 2805: Only export CAMLP4LIB if camlp4 -where ends successfullypboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15434 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-07Colorization of coqtop messages is turned *off* by defaultletouzey
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
2012-06-04A box to pretty-print them all.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15424 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-04Added a color output to Coqtop.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15421 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-04Separated notice vs info messages, and cleaned up the interface a bit.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15420 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-02Flushing formatters before program exit.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15415 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-01More cleaningppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15414 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-01Cleaning Pp.ppnl useppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15413 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-01Getting rid of Pp.msgnl and Pp.message.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15412 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-30Getting rid of Pp.msgppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15400 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-30More uniformisation in Pp.warn functions.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15399 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29Vernacexpr is now a mli-only file, locality stuff now in locality.mlletouzey
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
2012-05-23Revert copy/pasted function in to minilib thanks to clib.cmapboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15352 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-13Added semantic completion in CoqIDE. (Should also add an option for that...)ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15317 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-13Added a SearchAbout-like primitive in coqtop interface.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15313 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-13Added an interface primitive to ask coqtop for its internal versions.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15312 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-11Slightly modified the coqtop interface by adding an identifier inppedrot
goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15303 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02Always add the Coq_config.dirs to xdg_dirspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15265 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02Added an interface call to exit Coqtop nicely.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15263 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-26Program: avoid staying in program mode after a failed Program commandletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15247 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-15Adding newline after warning and restoring distinction betweenherbelin
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
2012-04-12lib directory is cut in 2 cma.pboutill
- 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
2012-04-05Shortcuts and optimizations of comparisonsxclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15118 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-30info_trivial, info_auto, info_eauto, and debug (trivial|auto)letouzey
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
2012-03-26Unification: Added a heuristic to solve problems of the formherbelin
?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
2012-03-20Reorganizing the structure of evarutil.ml (only restructuration, noherbelin
change of semantics). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15060 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-18Yet another subtlety with bug 2732: when several grammar rules of aherbelin
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
2012-03-14Second step of integration of Program:msozeau
- 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
2012-03-02Noise for nothingpboutill
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
2012-01-16make mli-doc fixpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14905 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-18CoqIde files position is freedesktop compliant.pboutill
Beware, it means that files position is not relative to coqtop position but is given by XDG_DATA_DIRS and XDG_CONFIG_DIRS. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14822 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-17Added ability to take the type of applied metas into account whenherbelin
instantiating them in the unification algorithm used for tactics. This allows to discard ill-typed uses of first-order unification which otherwise would have been fatal (this incidentally allows to partially restore some compatibility with 8.3 that was broken after eta was added in unification). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14812 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-28Finally used typing to decide whether an alias needs to be expanded orherbelin
not in pattern-matching compilation. Also extended to the Var case the preference given to using the term to match as alias rather than its expansion. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14737 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-25Cleaning up XML parsingppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14729 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-24Fixed the XML parser CDATA handling (and changed the EOL convention of these ↵ppedrot
files which where Windows-like, whoever knows why). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14726 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-24Moving XML handling to lib directoryppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14723 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-20coqrc in the right XDG_CONFIG_HOME/coq folderpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14696 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-20Add support for XDG_DATA_HOME and XDG_DATA_DIRS.pboutill
From Tom Prince git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14692 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-14Bug 2636 - Move string_of_ppcmds to Pppboutill
by Tom Prince git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14650 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-17Patch by Dan Grayson to ensure that "Add LoadPath ... as ..." closesherbelin
the file descriptors on directories that it does not need to keep open (the maximum number of simultaneously opened file descriptors supported by the operating system is not so large in practice, e.g. 256 on MacOS X). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14565 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-22 20:06:43 +0000