index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
firstorder
Commit message (
Expand
)
Author
Age
*
Vernacexpr is now a mli-only file, locality stuff now in locality.ml
letouzey
2012-05-29
*
Fixing bug #2732 (anomaly when using the tolerance for writing
herbelin
2012-03-18
*
Second step of integration of Program:
msozeau
2012-03-14
*
Noise for nothing
pboutill
2012-03-02
*
Added a DEPRECATED flag in declaration of options. For now only two options a...
ppedrot
2011-11-24
*
Merge subinstances branch by me and Tom Prince.
msozeau
2011-11-17
*
Fix bug #2227
msozeau
2011-10-18
*
Term: moved function constr_ord (a.k.a compare_constr) from Sequent to Term
puech
2011-07-29
*
Sequent: generic equality on global_reference replaced by RefOrdered.compare
puech
2011-07-29
*
Sequent: generic equality on kernel_name replaced by kn_ord
puech
2011-07-29
*
Sequent: generic equality on constr replaced by destructors
puech
2011-07-29
*
Sequent: generic equality on ident replaced by id_ord
puech
2011-07-29
*
Instances: generic equality on global_reference replaced by RefOrdered.compare
puech
2011-07-29
*
Unify: generic equality on constr replaced by eq_constr
puech
2011-07-29
*
ARGUMENT EXTEND: forbid TYPED simultaneously with {RAW,GLOB}_TYPED
glondu
2010-12-25
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-23
*
Minor fixes:
msozeau
2010-07-27
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Fixing spelling: pr_coma -> pr_comma
herbelin
2010-06-12
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Here comes the commit, announced long ago, of the new tactic engine.
aspiwack
2010-04-22
*
Add a generic tactic option builder. Use it in firstorder to set the
msozeau
2010-03-05
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
- Inductive types in the "using" option of auto/eauto/firstorder are
herbelin
2009-09-13
*
- 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