index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
pretyping.mllib
Commit message (
Expand
)
Author
Age
*
Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)
Pierre Letouzey
2014-03-02
*
Splitted Evarutil in two files
ppedrot
2013-02-10
*
New implementation of the conversion test, using normalization by evaluation to
mdenes
2013-01-22
*
correct some ends of .mllib files (avoid a broken tolink.ml)
letouzey
2012-08-24
*
Pattern as a mli-only file, operations in Patternops
letouzey
2012-05-29
*
Glob_term now mli-only, operations now in Glob_ops
letouzey
2012-05-29
*
locus.mli for occurrences+clauses, misctypes.mli for various little things
letouzey
2012-05-29
*
Second step of integration of Program:
msozeau
2012-03-14
*
Renamig support added to "Arguments"
gareuselesinge
2011-11-21
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Here comes the commit, announced long ago, of the new tactic engine.
aspiwack
2010-04-22
*
Added a function in typing.ml to solve evars of a constr w/o going back down ...
herbelin
2010-04-05
*
In "simpl c" and "change c with d", c can be a pattern.
herbelin
2009-12-24
*
A bit of cleaning around name generation + creation of dedicated file namegen.ml
herbelin
2009-11-09
*
Many changes in the Makefile infrastructure + a beginning of ocamlbuild
letouzey
2009-03-20