aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2012-09-20Fixing Show Script issues.ppedrot
2012-09-18Coq_makefile fixupspboutill
2012-09-18More cleaning in CArray...ppedrot
2012-09-18More cleanup of Util: utf8 aspects moved to a new file unicode.mlletouzey
2012-09-18Cleaning interface of Util.ppedrot
2012-09-17More cleaning on Utils and CList. Some parts of the code beingppedrot
2012-09-17MacOS integration uses lablgtkosx >= 1.1pboutill
2012-09-17More type-safe interface to Coq XML API.ppedrot
2012-09-16Move reflexivity, symmetry, and transitivity, next to f_equal, in the documen...gmelquio
2012-09-16Some more fixes to tactic documentation.gmelquio
2012-09-16Beautify tactic documentation a bit more.gmelquio
2012-09-16Remove superfluous spaces and commas in tactic documentation.gmelquio
2012-09-16Fix index generation for the pdf document.gmelquio
2012-09-15Fix failure to compile doc/stdlib/Library.tex.gmelquio
2012-09-15Port rewrites of tactic documentation from branch 8.4.gmelquio
2012-09-15Some documentation and cleaning of CList and Util interfaces.ppedrot
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-09-14Added some tricky tail-rec versions of List functions to CListppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-20 04:49:06 +0000