aboutsummaryrefslogtreecommitdiff
path: root/pretyping/pretyping.mllib
AgeCommit message (Expand)Author
2014-05-08Moving Dnet-related code to tactics/.Pierre-Marie Pédrot
2014-03-02Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)Pierre Letouzey
2013-02-10Splitted Evarutil in two filesppedrot
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-08-24correct some ends of .mllib files (avoid a broken tolink.ml)letouzey
2012-05-29Pattern as a mli-only file, operations in Patternopsletouzey
2012-05-29Glob_term now mli-only, operations now in Glob_opsletouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-03-14Second step of integration of Program:msozeau
2011-11-21Renamig support added to "Arguments"gareuselesinge
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
2010-04-05Added a function in typing.ml to solve evars of a constr w/o going back down ...herbelin
2009-12-24In "simpl c" and "change c with d", c can be a pattern.herbelin
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
2009-03-20Many changes in the Makefile infrastructure + a beginning of ocamlbuildletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 23:45:32 +0000