aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2012-10-04En cours pour bug 2836herbelin
2012-10-04Makefile.build: easier compilation with timings infoletouzey
2012-10-04Getting rid of Compat in the checker.ppedrot
2012-10-04Adding a nominal typing layer to Metasyntax in order to clarifyppedrot
2012-10-04Moved Compat to parsing. This permits to break the dependency of theppedrot
2012-10-02Remove the unused "intel" field in Proof.proof_stateletouzey
2012-10-02Remove some dead code in the vmletouzey
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-10-02Argextend: avoid useless "open Extrawit"letouzey
2012-10-02avoid referring to Term in constrexpr.mli and glob_term.mliletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-02 15:33:06 +0000