aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2012-10-02New makefile shortcuts miniopt and minibyte for coqtop + pluginsletouzey
2012-10-02Use the library function List.substract in prev commitletouzey
2012-10-01Added a new tactical infoH tac, that displays the names of hypothesis created...courtieu
2012-10-01Ltac repeat is in fact already doing progressletouzey
2012-09-27Default hashconsing of identifiers.ppedrot
2012-09-26Reusing the Hashset data structure in Hashcons. Hopefully, this shouldppedrot
2012-09-26Incorrect commentmsozeau
2012-09-26Cleaning, renaming obscure functions and documenting in Hashcons.ppedrot
2012-09-25Fixing ocamldoc errorsppedrot
2012-09-25Added a ml-dot option to Makefile to generate dependency graph of core modulesppedrot
2012-09-25Fixing #2865.ppedrot
2012-09-24Fixing a bug introduced in Funind plugin when reorganizing the CListppedrot
2012-09-22Fix use of $(HASNATDYNLINK) in coq_makefile outputglondu
2012-09-20Avoid generating ide/coqide_main*.ml as cleartext (except if READABLE_ML4 is ...letouzey
2012-09-20Remove broken makefile option NO_RECOMPILE_LIBletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-24 21:15:20 +0000