aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2012-11-12Removed the modification of the GC pressure coefficient, in orderppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-11-08Added an Int module with dummy utility functions.ppedrot
2012-11-08Removing another bunch of generic equalitiesppedrot
2012-11-07Fix reference_or_constr grammar rule to accept @t as a constrgareuselesinge
2012-11-06Coq is a heavy user of persistent data structures and symbolic ASTs, so theppedrot
2012-11-03Reversed roles of undefined/defined evars in Evd, thus saving preciousppedrot
2012-10-31Coqide Detach View: avoid doing gtk stuff in sub-thread (fix #2863)letouzey
2012-10-31Change [Hints Resolve] to still accept constrs as argumentsmsozeau
2012-10-31correcting a little bug in Functionjforest
2012-10-30Documenting the 'Printing Transparent/All Dependencies' command.ppedrot
2012-10-30Extraction Implicit: consider the parameters of a constructor (fix #2905)letouzey
2012-10-30Extraction: avoid initial strange empty comments after Arnaud's hackletouzey
2012-10-30Fix Separate extraction when a module-as-file is aliased (#2917)letouzey
2012-10-29coqdep: honor dependencies of "Load"ed filesgareuselesinge
2012-10-29Allow running coq-tex in win32 (fix #2921)letouzey
2012-10-29Fixed #2926:ppedrot
2012-10-29Removed many calls to OCaml generic equality. This was done byppedrot
2012-10-26Moved Entries module back to kernelppedrot
2012-10-26Change Hint Resolve, Immediate to take a global reference as argumentmsozeau
2012-10-24Removed a few calls to "Opaque" in Logic.v ineffective since at leastherbelin
2012-10-23Cleared a purely declarative .ml file and moved its interface to intf/ppedrot
2012-10-23Coqmktop: missing -I (fix #2851)letouzey
2012-10-23 the new .dir-locals.el thanks to Pierre Courtieupboutill
2012-10-23Text inserted by insert_this_phrase_on_success correct taggingpboutill
2012-10-23Coqide for Gtk-mac-integration 2.0.0pboutill
2012-10-23RefMan-tac: fix a few glitches concerning the documentation of eqn:letouzey
2012-10-22Fix bug #2892letouzey
2012-10-22Coqide does not need dllcoqrun.sopboutill
2012-10-17Makefile.build: CONFIG is now in clibpboutill
2012-10-17Do not install libcoqrun.so if compiled with -custompboutill
2012-10-17Cygwin gcc do not accept -mno-cygwin anymorepboutill
2012-10-17Fix test-suite output/* in benchpboutill
2012-10-17Taking into account that ocamlfind might find a package w/o the filesherbelin
2012-10-17Using weak tables instead of plain hash tables while hashconsing.ppedrot
2012-10-17univ inconsistency error message gives evidence of a cyclebarras
2012-10-16Removing redundant definition of case_eq (see #2919).herbelin
2012-10-16Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterpletouzey
2012-10-16Continuing r15885 fixing coqdoc index bugs introduced in r14624 and r15053.herbelin
2012-10-16Removed dead code about linking Module names in coqdoc.herbelin
2012-10-15Continue killing hidden tactics : no more generated h_xxxletouzey
2012-10-15Egramml: minor simplificationletouzey
2012-10-15Stylistic improvement: avoid a "if match List.hd"letouzey
2012-10-15Coq_makefile: easier compilation with timings info (from r15850)pboutill
2012-10-15Makefiles: Only -I required dirs (config, lib, ide) when compiling coqidepboutill
2012-10-15Makefile.build: $(MLINCLUDES) out of $(OPT/BYTEFLAGS)pboutill
2012-10-15Fixing coqdoc index bugs introduced in r14624 and r15053. Revision r14624 int...pboutill
2012-10-14When loading a plugin, prefer .cma to .cmogareuselesinge
2012-10-08fix r15860 : no slash after $(COQLIB)letouzey
2012-10-06restore compatibility with camlp5 < 6.00letouzey