aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/obligations.ml
Commit message (Expand)AuthorAge
* Getting rid of Pp.msgGravatar ppedrot2012-05-30
* More uniformisation in Pp.warn functions.Gravatar ppedrot2012-05-30
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
* Evar_kinds.mli containing former Evd.hole_kind, avoid deps on EvdGravatar letouzey2012-05-29
* Fix bugs related to Program integration.Gravatar msozeau2012-03-19
* Fix merge and add missing file.Gravatar msozeau2012-03-14
* Final part of moving Program code inside the main code. Adapted add_definitio...Gravatar msozeau2012-03-14