aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2012-10-06remove Refiner.abstract_tactic and similarletouzey
2012-10-06remove -rectypes except for term.mlletouzey
2012-10-06remove dumptree.ml4letouzey
2012-10-06Adapt pieces of code needing -rectypesletouzey
2012-10-06avoid using rectypes in dnet.mlletouzey
2012-10-06avoid using rectypes in nametab.mlletouzey
2012-10-06Tacexpr: revised version that doesn't need -rectypesletouzey
2012-10-06Clean-up : removal of Proof_type.tactic_exprletouzey
2012-10-06Proof_type: rule now degenerates to prim_ruleletouzey
2012-10-06Clean-up : no more Proof_type.proof_treeletouzey
2012-10-06Clean-up of proof_type.ml : no more Nested nor abstract_tactic_boxletouzey
2012-10-05Fix a confusion between types of locations in an untyped part of the parserletouzey
2012-10-05Repair the configure after Hugo's last "repair" ;-)letouzey
2012-10-05coqtop -time : display per-command timingsletouzey
2012-10-05More accurate timings for "Time foo"letouzey
2012-10-04Revert r15851 "En cours pour bug 2836".herbelin
2012-10-04Revert "En cours pour 'generalize in clause' et 'induction in clause'"herbelin
2012-10-04Repaired configure damaged in r15748 for those bash users which haveherbelin
2012-10-04Suggest to use clean rather than archclean before recompiling.herbelin
2012-10-04Improving error message when abtraction over goal (abstract_list_allherbelin
2012-10-04En cours pour 'generalize in clause' et 'induction in clause'herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 20:18:30 +0000