aboutsummaryrefslogtreecommitdiff
path: root/pretyping/pretyping.mllib
AgeCommit message (Expand)Author
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