aboutsummaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Collapse)Author
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
2011-10-10Hashtbl_alt : typo in a commentletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14541 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-27In Coq_config: get rid of coqsrc and make coqlib optionalglondu
I assume that once Coq is installed in non-local mode and run from its installed path, sources are no longer available. The coqsrc variable doesn't make any sense, then, and its intended value can always be inferred from Sys.executable_name. Moving it to Envars.coqroot. Make coqlib optional. Currently, it is set to None only in -local mode or with ocamlbuild. When set to None, -local layout is assumed (binaries in ./bin, library in .). The behaviour should not be changed when an explicit coqlib has been given to ./configure. This commit should make it possible to run a Coq compiled with -local from anywhere (no hard-coded absolute path embedded in the executables, intermediary step to bug #2565). It WILL BREAK settings re-using source trees after installation in non-local mode (are there actual use cases for that?). Hard-coded absolute paths still remain: - in the build system, so the need to re-run ./configure after moving the source tree is still expected for now; - in coqrunbyteflags, I think we are limited by ocaml itself; - docdir. All absolute paths should be removed, ultimately. As a side-effect, simplify computing of Envars.coqbin. I don't see any good reason to keep it as a function. Disclaimers: - initialization of Sys.executable_name is not consistent across all architectures; relying so much on it might trigger bugs. I'm pretty sure something will explode if one adds arbitrary symlinks on top of that; - ocamlbuild stuff not tested. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14500 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-05Util.error now creates UserError(_,msg) instead of UserError(str,str)letouzey
This only affects display of errors when flag -debug is used, and it avoids strange message like "Error: in msg: msg" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14450 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01[/]+ is equivalent to [/] in System and its copypboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14435 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-10Added list_map_filter_imsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14397 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Refl_omega: replaced some generic = on constr by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14355 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Coq_omega: replaced generic = on constr by eq_constrpuech
Util: Added list_assoc_f git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14350 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Hahtbl_alt: separate generic combine functionspuech
... and report changes on Term git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14344 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Evarutil: generic equality on constr replaced by eq_constr (x2)puech
added array_equal in Util git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14323 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Tactics: generic equality on constr replaced by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14321 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Term: Refactoring of hashconsingpuech
- moved the alterate Hashtable module to a separate file - moved all hashconsing-related function to a separate section in Term git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14312 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-22For the beauty of tail recursion, a new list_addnpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14289 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-16This option disables the use of the '{| field := ... |}' notationherbelin
when printing. Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14284 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-18Generalizing flag use_evars_pattern_unification into a flagherbelin
use_pattern_unification common for evars and metas. As a compensation, add a flag use_meta_bound_pattern_unification to restore the old mechanism of pattern unification for metas applied to rels only (this is used e.g. by auto). Not sure yet, what could be the most appropriate set of flags. Added documentation of the flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14221 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-24Made the emacs-U option deprecated. Also removed the old codecourtieu
inserting special chars for proof by pointing with emacs. This was interacting badly with utf8. It may be implemented back with xml-like tags instead of special chars. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14154 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-19Remove useless "open Gc"glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14146 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-19Remove System.process_time (dead code)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14145 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-17More work on error handlingletouzey
Anomalies are now meant to be the exceptions that are *not* catched and handled by the new Errors.handle_stack. Three variants of [Errors.print] allow to customize how anomalies are treated. In particular, [Errors.print_no_anomaly] is used for the Fail command, instead of a classification function Cerrors.is_user_error which wasn't customizable. No more AnomalyOnError, its only occurrence is now a regular anomaly git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14133 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-13A new mechanism to handle errors.aspiwack
Instead of the monolitic Cerrors, I introduce a lightweight Errors module whose error message can be expanded by module introducing exceptions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14119 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-29Choose relative directory over configured directory for coqlib.pboutill
This also fixes the bug where Util.error is always called, if coq searches for a relative directory. Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14084 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-28coqtop -config returns coq returns coq environments at exection timepboutill
It looks like a variables definition part of a Makefile. Names are from coq makefiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14080 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-21Win32: remove the need for Coq.bat and Coqide.batletouzey
This is an adaptation of commit r13750 of branch 8.3 - coqlib is currently computed relatively of Sys.executable_name, hence no need to set it manually - in Win32, better detection of user home dir : in System.ml, if HOME isn't set, we look now for HOMEDRIVE\HOMEPATH, and then for USERPROFILE - concerning PATH, in Win32 we now add coqbin (or the location of coqide) to PATH during the initialization. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14041 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-14Add directories in COQPATH to search path.herbelin
This is to allow users to install plugins when coq is installed system-wide. Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14001 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-03Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksletouzey
The recent experiment with -dont-load-proofs in the stdlib showed that this options isn't fully safe: some axioms were generated (Include ? functor application ? This is still to be fully understood). Instead, I've implemented an idea of Yann: only load opaque proofs when we need them. This is almost as fast as -dont-load-proofs (on the stdlib, we're now 15% faster than before instead of 20% faster with -dont-load-proofs), but fully compatible with Coq standard behavior. Technically, the const_body field of Declarations.constant_body now regroup const_body + const_opaque + const_inline in a ternary type. It is now either: - Undef : an axiom or parameter, with an inline info - Def : a transparent definition, with a constr_substituted - OpaqueDef : an opaque definition, with a lazy constr_substitued Accessing the lazy constr of an OpaqueDef might trigger the read on disk of the final section of a .vo, where opaque proofs are located. Some functions (body_of_constant, is_opaque, constant_has_body) emulate the behavior of the old fields. The rest of Coq (including the checker) has been adapted accordingly, either via direct access to the new const_body or via these new functions. Many places look nicer now (ok, subjective notion). There are now three options: -lazy-load-proofs (default), -force-load-proofs (earlier semantics), -dont-load-proofs. Note that -outputstate now implies -force-load-proofs (otherwise the marshaling fails on some delayed lazy). On the way, I fixed what looked like a bug : a module type (T with Definition x := c) was accepted even when x in T was opaque. I also tried to clarify Subtyping.check_constant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13952 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-05Starting being more explicit on the reasons why module subtyping fails.herbelin
Note: I'm unsure about some subtyping error case apparently involving aliases of inductive types (middle of Subtyping.check_inductive); I bound it to some NotEqualInductiveAliases error, but this has to be checked. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13885 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-14- Fix treatment of globality flag for typeclass instance hints (theymsozeau
were all declared as global). - Add possibility to remove hints (Resolve or Immediate only) based on the name of the lemma. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13842 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-11An generic imperative union-find, used for deps of evars in Class_tacticsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13831 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-31A fine-grain control of inlining at functor application via priority levelsletouzey
As said in CHANGES: << The inlining done during application of functors can now be controlled more precisely. In addition to the "!F G" syntax preventing any inlining, we can now use a priority level to select parameters to inline : "<30>F G" means "only inline in F the parameters whose levels are <= 30". The level of a parameter can be fixed by "Parameter Inline(30) foo". When levels aren't given, the default value is 100. One can also use the flag "Set Inline Level ..." to set a level. >> Nota : the syntax "Parameter Inline(30) foo" is equivalent to "Set Inline Level 30. Parameter Inline foo.", and "Include <30>F G" is equivalent to "Set Inline Level 30. Include F G." For instance, in ZBinary, eq is @Logic.eq and should rather be inlined, while in BigZ, eq is (fun x y => [x]=[y]) and should rather not be inlined. We could achieve this behavior by setting a level such as 30 to the parameter eq, and then tweaking the current level when applying functors. This idea of levels might be too restrictive, we'll see, but at least the implementation of this change was quite simple. There might be situation where parameters cannot be linearly ordered according to their "inlinablility". For these cases, we would need to mention names to inline or not at a functor application, and this is a bit more tricky (and might be a pain to use if there are many names). No documentation for the moment, since this feature is experimental and might still evolve. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13807 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
According to B. Gregoire, this stuff is obsolete. Fine control on when to launch the VM in conversion problems is now provided by VMcast. We were already almost never boxing definitions anymore in stdlib files. "(Un)Boxed Definition foo" will now trigger a parsing error, same with Fixpoint. The option "(Un)Set Boxed Definitions" aren't there anymore, but tolerated (as no-ops), since unknown options raise a warning instead of an error by default. Some more cleaning could be done in the vm. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13806 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-25Fix compilation with camlp5 (Closes: #2487)glondu
With hints from Daniel de Rauglaudre. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13802 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-06Remove Safe_marshalglondu
Safe_marshal was using intermediate strings that are subject to Sys.max_string_length limitation. Use directly binary channel-oriented functions instead. This is a fix for bug #2471. Remark: this might reduce robustness w.r.t. noise in the communication channel. AFAIK, the original purpose of Safe_marshal was to work around a bug on Windows... this should be investigated further. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13765 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-25Avoid "open {Pcoq,Extrawit}" clauses in expansion of EXTEND commandsglondu
It is quite nasty to insert those open in places where they can change the semantics of surrounding code... instead, prefer using fully-qualified names in generated code when possible. For ExtraArgType, simulate a "open Extrawit in ..." (which does exist primitively in OCaml >= 3.12) with the usual encoding. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13759 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-06Use !Pp_control.std_ft for printing grammarsglondu
With camlp5 6.02.1, this fixes "Print Grammar" in coqide. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13687 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-03Remove dead codeglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13669 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-18adapt slighlty r13642 to support both camlp4 and camlp5-5 and camlp5-6letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13652 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-16Support for camlp5 6.02.0 (Closes: #2432)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13642 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-03Added multiple implicit arguments rules per name.herbelin
Example: "Implicit Arguments eq_refl [[A] [x]] [[A]]". This should a priori be used with care (it might be a bit disturbing seeing the same constant used with apparently incompatible signatures). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13484 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
In particular, the unused lib/tlm.ml and lib/gset.ml are removed In addition, to simplify code, Libobject.record_object returning only the ('a->obj) function, which is enough almost all the time. Use Libobject.record_object_full if you really need also the (obj->'a). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13460 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-19Addressing part 2 of bug report 2377 (removing intrusive warning whenherbelin
coqide doc link is the canonical link to last released version of reference manual instead of link to corresponding coqide version). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13436 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 15:01:55 +0000