aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/lib.mli
Commit message (Expand)AuthorAge
* Update headers.Gravatar Maxime Dénès2015-01-12
* Removing dead code relative to the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* Fix Declaremods.end_library (Closes: #3536)Gravatar Enrico Tassi2014-09-02
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
* New compilation mode -vi2voGravatar Enrico Tassi2014-02-26
* Nicer code concerning dirpaths and modpath around LibGravatar letouzey2013-08-22
* enhance marshallable option for freeze (minor TODO in safe_typing)Gravatar gareuselesinge2013-08-08
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Lib.contents () instead of Lib.contents_after NoneGravatar letouzey2013-07-17
* Use the Hook module here and there.Gravatar ppedrot2013-05-12
* States: frozen states can hold closuresGravatar gareuselesinge2013-05-06
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Fix issues with "Reset Initial" in scripts given to coqtop -lGravatar letouzey2013-04-23
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Assumption commands are now displayed as unsafe in Coqide.Gravatar aspiwack2012-08-24
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* A unified backtrack mechanism, with a basic "Show Script" as side-effectGravatar letouzey2012-03-23
* Remove undocumented command "Delete foo"Gravatar letouzey2012-03-23
* Noise for nothingGravatar pboutill2012-03-02
* 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
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Various minor improvements of comments in mli for ocamldocGravatar letouzey2010-04-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Granting wish #2249 (checking existing lemma name also when in a section).Gravatar herbelin2010-04-09
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Backtrack on the forced discharge of type class variables introducedGravatar msozeau2009-09-14
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Fix implicit args code so that declarations are added for allGravatar msozeau2009-05-27
* - Synchronized subst_object with load_object (load_and_subst_objects)Gravatar herbelin2008-11-23
* broke cyclic dependenciesGravatar barras2008-07-24
* Correct implementation of discharging of implicit arguments and add newGravatar msozeau2008-07-22
* Documentation Prop<=Set et Arguments Scope GlobalGravatar herbelin2008-07-01
* Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...Gravatar notin2008-06-25
* Fix setoid_rewrite documentation examples.Gravatar msozeau2008-06-03
* - Prise en compte des frozen state de Coq autant que possible pourGravatar herbelin2008-05-24
* Correction bug #1842 + correction bug initialisation introduit dansGravatar herbelin2008-05-10
* - Prise en compte de l'unicode dans la fonction hdchar (elle fournissait desGravatar herbelin2008-05-10
* Add the ability to specify the implicit status of section variables andGravatar msozeau2008-04-02