| Age | Commit message (Expand) | Author |
|---|
| 2012-06-22 | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot |
| 2012-05-30 | Getting rid of Pp.msg | ppedrot |
| 2012-05-29 | Some documentation of recent changes concerning interfaces | letouzey |
| 2012-05-29 | place all pretty-printing files in new dir printing/ | letouzey |
| 2012-05-29 | Extend become a mli-only file in intf/ | letouzey |
| 2012-05-29 | Split Egrammar into Egramml and Egramcoq | letouzey |
| 2012-05-29 | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey |
| 2012-05-29 | Strongly reduce the dependencies of grammar.cma, modulo two hacks | letouzey |
| 2012-05-29 | 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 | Tacexpr as a mli-only, the few functions there are now in Tacops | letouzey |
| 2012-05-29 | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey |
| 2012-05-29 | Vernacexpr is now a mli-only file, locality stuff now in locality.ml | letouzey |
| 2012-04-27 | Coqide MacOS integration refresh | pboutill |
| 2012-04-12 | lib directory is cut in 2 cma. | pboutill |
| 2012-04-06 | Removing Dhyp from debugger. | herbelin |
| 2012-03-14 | Everything compiles again. | msozeau |
| 2012-03-02 | Noise for nothing | pboutill |
| 2012-02-01 | Debugger vs tracer: Two different behaviors wrt printing: The debugger | herbelin |
| 2012-01-20 | Added new command "Set Parsing Explicit" for deactivating parsing (and | herbelin |
| 2011-12-18 | Suspending declaration of undefined debug printers. | herbelin |
| 2011-11-21 | Renamig support added to "Arguments" | gareuselesinge |
| 2011-11-17 | Merge subinstances branch by me and Tom Prince. | msozeau |
| 2011-10-25 | First attempt at making Print Assumption compatible with opaque modules (fix ... | letouzey |
| 2011-10-17 | Revert "New evar_map printer ppevmfull which can typically be installed for" | herbelin |
| 2011-10-17 | New evar_map printer ppevmfull which can typically be installed for | herbelin |
| 2011-10-15 | dev/base_include: display a nice message at the end of the load | letouzey |
| 2011-10-15 | debugging.txt: no more typing of #use "include" if using .ocamlinit | letouzey |
| 2011-10-11 | Moved to a more standard order of arguments (i.e. env followed by evar_map) | herbelin |
| 2011-10-01 | Moving never-used comments from Zhints.v to dev/doc so as not to | herbelin |
| 2011-09-25 | Polishing commits r14492, r14448 and r14407 (tactics propagate | herbelin |
| 2011-08-04 | Fix unification: detect invalid evar instantiations due to scoping earlier. | msozeau |
| 2011-07-29 | Add printer dependency to Hashtbl_alt (used in Term) | puech |
| 2011-07-18 | Fixed a "feature" of "inversion" and "dependent rewrite" revealed by | herbelin |
| 2011-07-16 | Finally, pr_goal seems to work for printing v8.2 style goal in debugger. | herbelin |
| 2011-06-21 | Cleaning debugging printer relative to new proof engine. In | herbelin |
| 2011-06-13 | A few comments and a dev file to summarize issues with unification | herbelin |
| 2011-05-13 | A new mechanism to handle errors. | aspiwack |
| 2011-05-03 | As many notation for for vectors as for List. | pboutill |
| 2011-04-26 | dev/base_include: no more mod_self_id | letouzey |
| 2011-04-13 | - Remove create_evar_defs | msozeau |
| 2011-04-06 | Fix dev/base_include after change of constant_body | letouzey |
| 2011-03-16 | Adapt printers.mllib after my last commit | letouzey |
| 2011-02-11 | Annotations at functor applications: | letouzey |
| 2011-02-11 | Update changelogs | glondu |
| 2011-02-07 | Factorize code of rewrite to make way for a new implementation using the | msozeau |
| 2010-12-24 | Remove obsolete script univdot, update dev doc about universes | glondu |
| 2010-12-23 | Rename rawterm.ml into glob_term.ml | glondu |
| 2010-12-23 | Change of nomenclature: rawconstr -> glob_constr | glondu |
| 2010-12-23 | Prepare change of nomenclature rawconstr -> glob_constr | glondu |
