index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
omega
Commit message (
Expand
)
Author
Age
*
Fixed some missing options from previous commit.
ppedrot
2011-11-24
*
Omega: for non-arithmetical goals, try proving False from context (wish #2236)
letouzey
2011-09-16
*
Omega aware of Z.pred (fix #1912)
letouzey
2011-09-15
*
Improved ltac code for zify (fix #2575).
letouzey
2011-09-06
*
Coq_omega: replaced generic = on constr by eq_constr
puech
2011-07-29
*
Coq_omega: replaced many generic = on constr by eq_constr
puech
2011-07-29
*
Modularisation of Znat, a few name changed elsewhere
letouzey
2011-05-05
*
Modularization of Pnat
letouzey
2011-05-05
*
Modularization of BinPos + fixes in Stdlib
letouzey
2011-05-05
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Some more revision of {P,N,Z}Arith + bitwise ops in Ndigits
letouzey
2010-11-18
*
Use full path for unknown stuff in omega
glondu
2010-11-16
*
Remove some occurrences of "open Termops"
glondu
2010-09-28
*
Fix unescaped end-of-lines (OCaml warning 29)
glondu
2010-09-13
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Generic support for open terms in tactics
herbelin
2009-12-21
*
Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...
letouzey
2009-12-09
*
OrderedType implementation for various numerical datatypes + min/max structures
letouzey
2009-11-03
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
- Cleaning phase of the interfaces of libnames.ml and nametab.ml
herbelin
2009-08-06
*
Improved parameterization of Coq:
herbelin
2009-08-02
*
Many changes in the Makefile infrastructure + a beginning of ocamlbuild
letouzey
2009-03-20
*
Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...
letouzey
2009-03-20