aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2012-11-12Removed the modification of the GC pressure coefficient, in orderppedrot
to see if that really changes anything. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15958 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
the new Int module. Only the most obvious were removed, so there are a lot more in the wild. This may sound heavyweight, but it has two advantages: 1. Monomorphization is explicit, hence we do not miss particular optimizations of equality when doing it carelessly with the generic equality. 2. When we have removed all the generic equalities on integers, we will be able to write something like "let (=) = ()" to retrieve all its other uses (mostly faulty) spread throughout the code, statically. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15957 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-08Added an Int module with dummy utility functions.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15956 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-08Removing another bunch of generic equalitiesppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15955 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-07Fix reference_or_constr grammar rule to accept @t as a constrgareuselesinge
With the previous formulation extra parentheses had to be added, now they are only necessary for compound expressions, like an application. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15954 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-06Coq is a heavy user of persistent data structures and symbolic ASTs, so theppedrot
minor heap is heavily sollicited. Unfortunately, the default size is far too small, so we enlarge it a lot (128 times larger). To better handle huge memory consumers, we also augment the default major heap increment and the GC pressure coefficient. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15953 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-03Reversed roles of undefined/defined evars in Evd, thus saving preciousppedrot
time when requesting only undefined evars (which is actually most often the case, as in Goal.advance). Hopefully this should not disrupt anything. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15952 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-31Coqide Detach View: avoid doing gtk stuff in sub-thread (fix #2863)letouzey
In Win32, playing with gtk stuff outside gtk's main loop causes coqide to crash: we should be careful when using do_if_not_computing and its Thread.create. In the case of Detach View anyway, the do_if_not_computing was clearly useless. Strangely, the unix gtk seems more resilient and was not crashing ... Btw, avoid maintaining a thread-unsafe list of detached_views, use instead gtk callbacks to close detached views when their corresponding buffer in the main window is closed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15950 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-31Change [Hints Resolve] to still accept constrs as argumentsmsozeau
to maintain compatibility, the term is then declared as a constant internally. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15948 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-31correcting a little bug in Functionjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15947 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-30Documenting the 'Printing Transparent/All Dependencies' command.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15946 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-30Extraction Implicit: consider the parameters of a constructor (fix #2905)letouzey
The parameters of a constructor C are part of the type of C, we should take them in account when retrieving the argument(s) declared as implicit. This way, the Extraction Implicit should now be correct when given named arguments of constructors with parameters. When positional numbers are given to Extraction Implicit, these numbers should now be increased by the number of parameters for this constructor. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15943 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-30Extraction: avoid initial strange empty comments after Arnaud's hackletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15942 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-30Fix Separate extraction when a module-as-file is aliased (#2917)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15940 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-29coqdep: honor dependencies of "Load"ed filesgareuselesinge
Imagine A.v "Load"s B.v and that B.v "Require"s C. Before this commit we get: A.vo: A.v B.v After this commit we get: A.vo: A.v B.v C.vo git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15939 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-29Allow running coq-tex in win32 (fix #2921)letouzey
Yes, it seems that < and > and even 2>&1 are legal under windows :-) Btw, the only function using streams has been rewritten, so coq_tex is now a standard .ml file, not a .ml4 anymore (beware during upgrade!) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15938 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-29Fixed #2926:ppedrot
Extend "Print Opaque Dependencies" for transparent dependencies as well git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15935 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-29Removed many calls to OCaml generic equality. This was done byppedrot
writing our own comparison functions, and enforcing monomorphization in many places. This should be more efficient, btw. Still a work in progress. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15932 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-26Moved Entries module back to kernelppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15931 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-26Change Hint Resolve, Immediate to take a global reference as argumentmsozeau
instead of a general constr: this is the most common case and does not loose generality (one can simply define constrs before Hint Resolving them). Benefits: - Natural semantics for typeclasses, not class resolution needed at Hint Resolve time, meaning less trouble for users as well. - Ability to [Hint Remove] any hint so declared. - Simplifies the implementation as well. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15930 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-24Removed a few calls to "Opaque" in Logic.v ineffective since at leastherbelin
V7.1. Thanks to Assia for reporting. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15929 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-23Cleared a purely declarative .ml file and moved its interface to intf/ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15928 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-23Coqmktop: missing -I (fix #2851)letouzey
The modules used in coqmktop's temporary main file should have their .cmi in the search path, hence a small set of -I is required: lib, toplevel. We do not place their the full list to avoid issues with the win32 command-line length Btw, coqmktop -boot now also builds its list of -I instead of receiving them via its command-line, it's simpler this way... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15926 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-23 the new .dir-locals.el thanks to Pierre Courtieupboutill
As it says : Set default directory to coq root ONLY IF variable coq-project-find-file is non nil. This should remain a user preference and not be set by default. This setting is redundant with compile-command above as M-x compile always CD's to default directory. To enable it add this to your emacs config: (setq coq-project-find-file t) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15924 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-23Text inserted by insert_this_phrase_on_success correct taggingpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15923 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-23Coqide for Gtk-mac-integration 2.0.0pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15922 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-23RefMan-tac: fix a few glitches concerning the documentation of eqn:letouzey
These were introduced during Guillaume's backport to trunk of its improved tactic documentation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15920 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-22Fix bug #2892letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15916 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-22Coqide does not need dllcoqrun.sopboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15914 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-17Makefile.build: CONFIG is now in clibpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15909 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-17Do not install libcoqrun.so if compiled with -custompboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15908 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-17Cygwin gcc do not accept -mno-cygwin anymorepboutill
As far as I understand, the standard gcc in cygwin is not able anymore to build non cygwin executable. There is instead a special package with a special gcc that compiles executable that can be used out of cygwin. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15907 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-17Fix test-suite output/* in benchpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15906 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-17Taking into account that ocamlfind might find a package w/o the filesherbelin
needed for compiling being present. Do the check by hand. Incidentally improved reporting messages. Also check gSourceview.cmi rather than gSourceview.mli for better guess that lablgtk sourceview bindings are there (I've seen installations where gSourceview.mli was here but not gSourceview.cmi). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15901 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-17Using weak tables instead of plain hash tables while hashconsing.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15899 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-17univ inconsistency error message gives evidence of a cyclebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15898 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-16Removing redundant definition of case_eq (see #2919).herbelin
Thanks to F. Blanqui for spotting it out. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15897 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-16Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterpletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15896 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-16Continuing r15885 fixing coqdoc index bugs introduced in r14624 and r15053.herbelin
Indeed r15885 still had problems (index contained referenced objects and not only defined objects, sorry). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15893 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-16Removed dead code about linking Module names in coqdoc.herbelin
Code was probably unused since scan_file made obsolete in r11024. See also r12890. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15892 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-15Continue killing hidden tactics : no more generated h_xxxletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15891 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-15Egramml: minor simplificationletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15890 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-15Stylistic improvement: avoid a "if match List.hd"letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15889 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-15Coq_makefile: easier compilation with timings info (from r15850)pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15888 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-15Makefiles: Only -I required dirs (config, lib, ide) when compiling coqidepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15887 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-15Makefile.build: $(MLINCLUDES) out of $(OPT/BYTEFLAGS)pboutill
Allow to erase special $(CHKFLAGS) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15886 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-15Fixing coqdoc index bugs introduced in r14624 and r15053. Revision r14624 ↵pboutill
introduced bug #2709 on duplicate entries in index and tentative fix of it in r15053 mixed up names of files and names of constants in index (as reported by P. Castéran on coqdev). Patch by Hugo Herbelin :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15885 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-14When loading a plugin, prefer .cma to .cmogareuselesinge
Imagine foo.cma contains foo_utils.cmo and foo.cmo. Also imagine that foo.cmo depends on foo_utils.cmo. With this patch, when asked to load foo, Coq loads the foo.cma archive. Loading simply foo.cmo would fail since foo_utils.cmo is needed to load foo.cmo. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15883 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-08fix r15860 : no slash after $(COQLIB)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15882 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-06restore compatibility with camlp5 < 6.00letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15881 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 15:49:17 +0000