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