aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Updated Exninfo to the new Store type.Gravatar ppedrot2013-03-12
* Allowing different types of, not to be mixed, generic Stores throughGravatar ppedrot2013-03-12
* Allowing (Co)Fixpoint to be defined local and Let-style.Gravatar ppedrot2013-03-11
* Obligations generated by Program are now local.Gravatar ppedrot2013-03-11
* Documentation of the "Local Definition" command.Gravatar ppedrot2013-03-11
* Added a Local Definition vernacular command. This type of definitionGravatar ppedrot2013-03-11
* catch failures of pr_vernac to make -time failsafeGravatar gareuselesinge2013-03-08
* Use with_state_protection in pr_module_vardeclsGravatar gareuselesinge2013-03-08
* More monomorphization.Gravatar ppedrot2013-03-05
* Missing primitive in CArrayGravatar ppedrot2013-03-05
* compare_stack_shape before ise_stack2 in evar_convGravatar pboutill2013-02-28
* Repairing r16205: errors raised by check_evar_instance were no longerGravatar herbelin2013-02-28
* More informative error when a global reference is used in a context ofGravatar herbelin2013-02-28
* Coqlib: minor simplificationsGravatar letouzey2013-02-27
* Update debug code according to reorganization into modules.Gravatar msozeau2013-02-27
* Minor cleanup around Term_typingGravatar letouzey2013-02-27
* remove a warning after Drop about print_hint_dbGravatar letouzey2013-02-27
* Adapt dev/base_include to new DeclarationsGravatar letouzey2013-02-27
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
* Names: shortcuts for building {kn, constant, mind} with empty sectionsGravatar letouzey2013-02-26
* Names: Modularize constant and mutual_inductiveGravatar letouzey2013-02-26
* Mod_subst: misc reformulationsGravatar letouzey2013-02-26
* cbn friendly VectorDefGravatar pboutill2013-02-25
* Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo...Gravatar pboutill2013-02-25
* CoqIDE: Add TAB key to autocompleteGravatar ppedrot2013-02-25
* Fixing bug #2466Gravatar ppedrot2013-02-24
* New -no-native-compiler flag for configure, globally disabling the nativeGravatar mdenes2013-02-24
* Reduced the noise level when dynlinking in bytecode mode or whenGravatar mdenes2013-02-24
* Tentative heuristic fix to handle lexer failures from CoqIDE whenGravatar ppedrot2013-02-22
* Cosmetic changes to CoqIDE finder widget.Gravatar ppedrot2013-02-22
* Names: con_modpath and con_label access back the user kn partGravatar letouzey2013-02-21
* Added missing documentation of Set Printing Existential Instances.Gravatar herbelin2013-02-21
* A slightly more efficient test of well-typedness of restriction ofGravatar herbelin2013-02-21
* Added Evarsolve to the list of modules to open for debugging.Gravatar herbelin2013-02-21
* Fixing an annoying bug in CoqIDE which causes the very first lineGravatar ppedrot2013-02-20
* Fixing #2763Gravatar ppedrot2013-02-20
* More handling of scrollbars in CoqIDE completionGravatar ppedrot2013-02-20
* CoqIDE: Including autocompletion in word proposalsGravatar ppedrot2013-02-20
* Corrects bug #2959 (error during Qed leads to assertion failure).Gravatar aspiwack2013-02-20
* Adding scrollbars to CoqIDE autocompletionGravatar ppedrot2013-02-20
* New autocompletion mechanism in CoqIDE. Now provides many answersGravatar ppedrot2013-02-19
* avoid (Int.equal (cmp ...) 0) when a boolean equality existsGravatar letouzey2013-02-19
* Dir_path --> DirPathGravatar letouzey2013-02-19
* module_path --> ModPath.t, kernel_name --> KerName.tGravatar letouzey2013-02-19
* Mod_subst: an extra assertGravatar letouzey2013-02-19
* Classops : avoid some use of GmapGravatar letouzey2013-02-19
* Names: revised representation of constants and mutual_inductiveGravatar letouzey2013-02-19
* Mod_subst: improve sharing during kn substitutionsGravatar letouzey2013-02-18
* Removing Exc_located and using the new exception enrichementGravatar ppedrot2013-02-18
* Adding more primitives to ExninfoGravatar ppedrot2013-02-18