aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.mllib
Commit message (Expand)AuthorAge
* Moved code for finding subterms (pattern, induction, set, generalize, ...)Gravatar Hugo Herbelin2014-06-28
* Made the subterm finding function make_abstraction independent of theGravatar Hugo Herbelin2014-06-28
* Moving Dnet-related code to tactics/.Gravatar Pierre-Marie Pédrot2014-05-08
* Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)Gravatar Pierre Letouzey2014-03-02
* Splitted Evarutil in two filesGravatar ppedrot2013-02-10
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* correct some ends of .mllib files (avoid a broken tolink.ml)Gravatar letouzey2012-08-24
* Pattern as a mli-only file, operations in PatternopsGravatar letouzey2012-05-29
* Glob_term now mli-only, operations now in Glob_opsGravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Second step of integration of Program:Gravatar msozeau2012-03-14
* Renamig support added to "Arguments"Gravatar gareuselesinge2011-11-21
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Added a function in typing.ml to solve evars of a constr w/o going back down ...Gravatar herbelin2010-04-05
* In "simpl c" and "change c with d", c can be a pattern.Gravatar herbelin2009-12-24
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20