| Age | Commit message (Expand) | Author |
|---|
| 2012-05-29 | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey |
| 2012-05-29 | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey |
| 2012-03-23 | A unified backtrack mechanism, with a basic "Show Script" as side-effect | letouzey |
| 2012-03-23 | Remove undocumented command "Delete foo" | letouzey |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-11-02 | Add type annotations around all calls to Libobject.declare_object | letouzey |
| 2011-09-15 | Names.make_mbid and co : convert from/to identifier (avoid some String.copy) | letouzey |
| 2011-09-05 | Coqide: new backtracking code, based on the Backtrack command | letouzey |
| 2011-09-05 | Lib: remove strange code about backtracking to the current state | letouzey |
| 2011-09-05 | Lib.node: merge OpenedModtype and OpenedModule, same for Closed... | letouzey |
| 2010-09-24 | Some dead code removal, thanks to Oug analyzer | letouzey |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-05-05 | Patch bug 2313. | soubiran |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-09 | Granting wish #2249 (checking existing lemma name also when in a section). | herbelin |
| 2010-02-12 | Simplify backtracking | vgross |
| 2010-02-12 | Fixing closing of segments. | vgross |
| 2009-11-11 | Fixed bug #2168 (closing a section may have as side-effect the erasure | herbelin |
| 2009-10-21 | This big commit addresses two problems: | soubiran |
| 2009-10-08 | Fixed a bug introduced in revision 12265. | herbelin |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-09-14 | Backtrack on the forced discharge of type class variables introduced | msozeau |
| 2009-08-13 | Death of "survive_module" and "survive_section" (the first one was | herbelin |
| 2009-08-06 | - Cleaning phase of the interfaces of libnames.ml and nametab.ml | herbelin |
| 2009-05-29 | Fix extract hyps to correctly discharge all hyps as described by keep | msozeau |
| 2009-05-27 | Fix implicit args code so that declarations are added for all | msozeau |
| 2009-01-07 | Uniformisation of some error messages + added test on setoid rewrite. | herbelin |
| 2008-11-23 | - Synchronized subst_object with load_object (load_and_subst_objects) | herbelin |
| 2008-07-24 | broke cyclic dependencies | barras |
| 2008-07-22 | Correct implementation of discharging of implicit arguments and add new | msozeau |
| 2008-07-01 | Documentation Prop<=Set et Arguments Scope Global | herbelin |
| 2008-06-25 | Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio... | notin |
| 2008-05-24 | - Prise en compte des frozen state de Coq autant que possible pour | herbelin |
| 2008-05-10 | Correction bug #1842 + correction bug initialisation introduit dans | herbelin |
| 2008-04-02 | Add the ability to specify the implicit status of section variables and | msozeau |
| 2008-02-22 | Merge with lmamane's private branch: | lmamane |
| 2008-02-01 | Beaoucoup de changements dans la representation interne des modules. | soubiran |
| 2007-12-06 | Plus de combinateurs sont passés de Util à Option. Le module Options | aspiwack |
| 2007-12-05 | Factorisation des opérations sur le type option de Util dans un module | aspiwack |
| 2007-10-29 | Amélioration du message d'erreur dans end_module, end_module_type et close_s... | notin |
| 2007-01-10 | Merge with Lionel Elie Mamane's private branch: | lmamane |
| 2007-01-10 | Merge from Lionel Elie Mamane's private branch: | lmamane |
| 2007-01-10 | Nouvelle approche pour le discharge modulaire | herbelin |
| 2006-12-28 | Cleaning backtracking code, optimized "Backtrack n x y" when n is | courtieu |
| 2006-09-12 | Indentation + svnprop | notin |
| 2006-09-01 | Indentation + typo | notin |
| 2006-05-23 | Modification de add_glob (support des modules dans Coqdoc) | notin |
| 2006-05-23 | Clarification role de library_part : renommage en remove_section_part | herbelin |
| 2006-04-27 | Standardisation nom option_app en option_map | herbelin |
| 2005-12-23 | Vérification qu'un module est ouvert avant d'insérer une déclaration nommÃ... | herbelin |
