| Commit message (Expand) | Author | Age |
* | ocamlbuild: many improvements (macos 10.5 fix, correct dllpath, etc) | letouzey | 2009-03-29 |
* | Avoid inadvertent declaration of "on" as a keyword. New syntax is | msozeau | 2009-03-29 |
* | Fix useless redeclaration of a tactic name when UpdateTac is replayed. | msozeau | 2009-03-28 |
* | Rewrite of Program Fixpoint to overcome the previous limitations: | msozeau | 2009-03-28 |
* | Fix bug #2056 (discharge bug). | msozeau | 2009-03-28 |
* | Fix static compilation of numeral syntax (typo in _mod files, sorry ...) | letouzey | 2009-03-28 |
* | ZArith/Int: no need to load romega here (but rather in FullAVL) | letouzey | 2009-03-28 |
* | ZMicromega: useless dependency toward ZArith.Int | letouzey | 2009-03-28 |
* | Coqdep: some dead code and code move (first experiment with Oug) | letouzey | 2009-03-27 |
* | Parsing files for numerals (+ ascii/string) moved into plugins | letouzey | 2009-03-27 |
* | Remove unused mli files | letouzey | 2009-03-27 |
* | GroebnerZ: no more admitted lemmas | letouzey | 2009-03-27 |
* | Ocamlbuild: 1st reasonably complete version (rules for binaries + plugins + vo) | letouzey | 2009-03-26 |
* | Fixes in Program well-founded definitions: | msozeau | 2009-03-26 |
* | ocamlbuild: coqide, coqchk, a bit of .vo | letouzey | 2009-03-26 |
* | Coqdep_boot: one line with bad indentation | letouzey | 2009-03-26 |
* | Protect typeset arguments in titles in LaTeX output (fixes compilation | msozeau | 2009-03-26 |
* | clean revision and coqdep_boot, too | lmamane | 2009-03-26 |
* | bin/coq-{parser,interface}: use this coqtop, not the first in $PATH | lmamane | 2009-03-26 |
* | make coqdep_boot in stage1, not stage2 | lmamane | 2009-03-25 |
* | Fix coqdoc bugs reported by Ian Lynagh. | msozeau | 2009-03-24 |
* | ocamlbuild improvements + minor makefile fix | letouzey | 2009-03-24 |
* | pretty.mll of coqdoc becomes cpretty.mll (avoid clash with a camlp5 file) | letouzey | 2009-03-24 |
* | - Fixed bug 2058 (as much as possible - the syntax of "pose (f binders := ...)" | herbelin | 2009-03-23 |
* | Backport from v8.2 branch of 11986 (interpretation of quantified | herbelin | 2009-03-22 |
* | Compromise wrt introduction-names compatibility issue after addition | herbelin | 2009-03-22 |
* | More elaborate handling of newlines in Gallina mode. Support inline | msozeau | 2009-03-22 |
* | coqdoc fixes and support for parsing regular comments (request by | msozeau | 2009-03-22 |
* | Many changes in the Makefile infrastructure + a beginning of ocamlbuild | letouzey | 2009-03-20 |
* | Makefile: avoid $(ML4FILES:.ml4=.ml) since this is $(ML4FILESML) | letouzey | 2009-03-20 |
* | replaced dir_load by load_file because dir_load does not raise an exception w... | barras | 2009-03-20 |
* | delete contrib dirs | barras | 2009-03-20 |
* | Fixes to make Ynot compile with the trunk: | msozeau | 2009-03-20 |
* | Compatibility with Apple's non-gnu sed. | msozeau | 2009-03-20 |
* | Directory 'contrib' renamed into 'plugins', to end confusion with archive of ... | letouzey | 2009-03-20 |
* | coq_makefile: -c and -shared conflict; tacinterp: delay evaluation of tactic ... | barras | 2009-03-19 |
* | renamed %-mod.ml into %_mod.ml to avoid ocaml warning | barras | 2009-03-18 |
* | fixed ring/field warning about hyp cleaning up | barras | 2009-03-18 |
* | removed correctness dirs | barras | 2009-03-18 |
* | coq_makefile: no ml dependency on coq sources | barras | 2009-03-18 |
* | Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl) | herbelin | 2009-03-17 |
* | - gros commit sur ring et field: passage des arguments simplifie | barras | 2009-03-17 |
* | Makefile:clean: rm *-mod.ml | barras | 2009-03-17 |
* | - configure: affiche si le natdynlink est positionne | barras | 2009-03-17 |
* | missing -c option of ocamlc in coq_makefile; coqdep_boot main loop was includ... | barras | 2009-03-16 |
* | coqdep_boot: a specialized and dependency-free coqdep for killing one of the ... | letouzey | 2009-03-16 |
* | Makefile: fix ignored errors, several attempts to clarify things | letouzey | 2009-03-16 |
* | Makefile: minor improvements | letouzey | 2009-03-16 |
* | Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4" | herbelin | 2009-03-16 |
* | Cleaning/uniformizing the interface of tacticals.mli | herbelin | 2009-03-14 |