index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
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
*
Better mechanism for loading initial plugins
letouzey
2009-03-14
*
RefMan: a label defined twice
letouzey
2009-03-14
*
Makefile: ml dependencies of contribs are moved to .mllib files
letouzey
2009-03-14
*
Coqdep: better handling of Declare ML Module (via .mllib) + many cleanups
letouzey
2009-03-14
*
Coqdep: remove references to obsolete .zi and Require Implementation stuff
letouzey
2009-03-14
*
Cleanup: avoid the warning about Coq-tex not being a valid Ocaml module name
letouzey
2009-03-11
*
Cleanup: remove unused config/giveostype.ml
letouzey
2009-03-11
*
Cleanup: remove 3 unused files in ide/
letouzey
2009-03-11
*
Cleanup: remove old correctness files, unused for a long time
letouzey
2009-03-11
*
in natdynlink, lack of uniformity between general %.vo and Init/%.vo rules re...
barras
2009-03-09
*
Optionally list opaque constants in addition to axions/variables in
msozeau
2009-03-09
*
- per session coq command stack
vgross
2009-03-07
*
fixed groebner as a plugin + pattern matching Timeout
barras
2009-03-06
*
missing Require
barras
2009-03-06
*
oups (module Entiers remplace par Big_int)
barras
2009-03-06
*
ajout de la tactique groebner de Loic Pottier
barras
2009-03-05
*
illegal tactic application was having Ltac interpreter loop
barras
2009-03-04
*
doc et CHANGES pour la commande Timeout
barras
2009-03-04
*
removed unused state file
barras
2009-03-04
*
Timeout message was not always displayed
barras
2009-03-04
*
commande Timeout + compaction des traces de debug_tactic
barras
2009-03-04
*
Backtrack sur la mémoïsation de nf_evar.
aspiwack
2009-03-04
*
Temporary hack to make coqide.byte work (backport r11948) (see #2062)
glondu
2009-03-04
*
fixes to typecheck with old lablgtk.
vgross
2009-03-04
*
Hack to fix compilation problems. will be removed on lablgtk upgrade.
vgross
2009-03-03
*
porting r11900 11905 and 11953 to trunk
barras
2009-03-02
*
Heavy modifications on the widget and edition tab creation mechanism.
vgross
2009-03-02
*
=?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...
aspiwack
2009-02-27
*
extraction: update of README+CHANGES, rm of BUGS+TODO
letouzey
2009-02-27
*
Makefile: avoid building an empty contrib.cmxa
letouzey
2009-02-27
[next]