aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Expand)AuthorAge
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Getting rid of Pp.msgnl and Pp.message.Gravatar ppedrot2012-06-01
* Getting rid of Pp.msgGravatar ppedrot2012-05-30
* More uniformisation in Pp.warn functions.Gravatar ppedrot2012-05-30
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
* 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
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Decl_kinds becomes a pure mli file, remaining ops in new file kindops.mlGravatar letouzey2012-05-29
* lib directory is cut in 2 cma.Gravatar pboutill2012-04-12
* Module names and constant/inductive names are now in two separate namespacesGravatar letouzey2012-03-26
* A unified backtrack mechanism, with a basic "Show Script" as side-effectGravatar letouzey2012-03-23
* Remove undocumented command "Delete foo"Gravatar letouzey2012-03-23
* Fixing alpha-conversion bug #2723 introduced in r12485-12486.Gravatar herbelin2012-03-20
* Noise for nothingGravatar pboutill2012-03-02
* Implement the substitution function for global options. Fixes anomaly in ssre...Gravatar msozeau2012-02-23
* sequel of previous commitGravatar letouzey2011-12-21
* Isolate a few types of Goptions in a pure .mli, solving a dep issue with ocam...Gravatar letouzey2011-12-21
* Fixed a Not_found bug when declaring in a section some implicitGravatar herbelin2011-12-18
* A pass on warning printings. Made systematic the use of msg_warning soGravatar herbelin2011-12-17
* Proof using ...Gravatar gareuselesinge2011-12-12
* Minor fixes to ArgumentsGravatar gareuselesinge2011-12-06
* Added a function to inspect current option state.Gravatar ppedrot2011-11-24
* Added a DEPRECATED flag in declaration of options. For now only two options a...Gravatar ppedrot2011-11-24
* Renamig support added to "Arguments"Gravatar gareuselesinge2011-11-21
* New Arguments vernacularGravatar gareuselesinge2011-11-21
* Adding the type infrastructure to handle properly API management of optionsGravatar ppedrot2011-11-18
* Add type annotations around all calls to Libobject.declare_objectGravatar letouzey2011-11-02
* First attempt at making Print Assumption compatible with opaque modules (fix ...Gravatar letouzey2011-10-25
* Heads: avoid potentially uncaught Not_found via an assert falseGravatar letouzey2011-10-24
* Temporary revert commit 14550 since it breaks a few contribsGravatar letouzey2011-10-12
* in heads.ml, at least turn the Not_found of #2608 into assert falseGravatar letouzey2011-10-11
* Various simplifications about constant_of_delta and mind_of_deltaGravatar letouzey2011-10-11
* Rely on kernel to know if a name is already used so as to be consistent with it.Gravatar herbelin2011-10-08
* Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).Gravatar herbelin2011-10-05
* Completing r14448 and thus continuing r14407 (using Cast to propagateGravatar herbelin2011-09-24
* Hash-consing: attempt to stop hash-consing separately constr in declare.mlGravatar letouzey2011-09-22
* Names.make_mbid and co : convert from/to identifier (avoid some String.copy)Gravatar letouzey2011-09-15
* Coqide: new backtracking code, based on the Backtrack commandGravatar letouzey2011-09-05
* Lib: remove strange code about backtracking to the current stateGravatar letouzey2011-09-05
* Lib.node: merge OpenedModtype and OpenedModule, same for Closed...Gravatar letouzey2011-09-05
* Heads: generic equality on constr replaced by destructorGravatar puech2011-07-29
* Modops: the strengthening functions can work without any env argumentGravatar letouzey2011-05-17
* Print Module (Type) M now tries to print more detailsGravatar letouzey2011-05-11
* Revert "Add [Polymorphic] flag for defs"Gravatar msozeau2011-04-13
* Add [Polymorphic] flag for defsGravatar msozeau2011-04-13
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
* Goptions: repair Unset for int optionsGravatar letouzey2011-03-17
* Added a table for using reserved names for binding names to typesGravatar herbelin2011-03-05
* Annotations at functor applications:Gravatar letouzey2011-02-11