aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2012-10-06Coqmktop: a misplaced Filename.quote prevented temp file cleanupletouzey
2012-10-06Turn mltop.ml4 into a regular ocaml fileletouzey
2012-10-06ocamlbuild simplificationsletouzey
2012-10-06Minor fix in the ./build wrapper for ocamlbuildletouzey
2012-10-06no need for camlp4 cma's in coq misc toolsletouzey
2012-10-06still some more dead code removalletouzey
2012-10-06remove useless hidden_flag in TacMutual(Co)Fixletouzey
2012-10-06cosmetic concerning interp of TacShowHypsletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 17:59:07 +0000