aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* Revert "Add [Polymorphic] flag for defs"Gravatar msozeau2011-04-13
* - Remove create_evar_defsGravatar msozeau2011-04-13
* Fix merge.Gravatar msozeau2011-04-13
* - Do not make constants with an assigned type polymorphic (wrong unfoldings).Gravatar msozeau2011-04-13
* Add [Polymorphic] flag for defsGravatar msozeau2011-04-13
* Subtyping: align coqtop behavior concerning opaque csts on coqchk's oneGravatar letouzey2011-04-12
* Replaced printing number of ill-typed branch by printing name of constructorGravatar herbelin2011-04-08
* A few extra combinators about rel_declaration/named_declaration + a bit of docGravatar herbelin2011-04-06
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
* CHANGES: a word about recent changes in coqide, about Ctrl-C in vmGravatar letouzey2011-04-01
* Checks for signals in VM, allowing it to be interrupted by Ctrl-C (experimental)Gravatar letouzey2011-04-01
* Tentative to make unification check types at every instanciation of anGravatar msozeau2011-03-11
* adding eta in the vmGravatar bgregoir2011-03-08
* Moving printing of module typing errors upwards to himsg.ml so as toGravatar herbelin2011-03-05
* Starting being more explicit on the reasons why module subtyping fails.Gravatar herbelin2011-03-05
* Fixed a "feature" about subtyping records: one was expected not onlyGravatar herbelin2011-03-05
* Mod_subst: improving sharing of subst_mpsGravatar letouzey2011-02-24
* Some more simplification in Mod_substGravatar letouzey2011-02-23
* - Use transparency information all the way through unification andGravatar msozeau2011-02-17
* Mod_typing: some refactoring (common parts about MSEapply and co)Gravatar letouzey2011-02-11
* Safe_typing: some refactoring (avoiding copy-paste of record definitions)Gravatar letouzey2011-02-11
* Mod_subt: some more refactoring, substitution is also separated in two tablesGravatar letouzey2011-02-11
* Mod_subst: split delta_resolver in two tables (mp / kn)Gravatar letouzey2011-02-11
* compatibility <3.12 (Map.exists Map.singleton)Gravatar pboutill2011-02-11
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* Make simpl use the proper constant when folding (mutual) fixpointsGravatar letouzey2011-01-27
* Rewrite sort_universes to minimize the number of universesGravatar glondu2011-01-25
* In univ.ml, put universe_level primitives in its their own sub-moduleGravatar glondu2011-01-11
* Add "Print Sorted Universes"Gravatar glondu2011-01-11
* More coherent comment orderingGravatar glondu2011-01-11
* Fixing bug #2454: inversion predicate strategy for inferring the typeGravatar herbelin2010-12-19
* Univ: try to avoid a few lookup in the universe graphGravatar letouzey2010-12-18
* Univ.constraints made fully abstract instead of being a Set of abstract stuffGravatar letouzey2010-12-18
* Revert last commit 13723 on Univ : minor gains and more complex codeGravatar letouzey2010-12-18
* Univ: an attempt to lazily compact chains of Equiv in a functionnal wayGravatar letouzey2010-12-17
* Univ: two improvements (speed + space)Gravatar letouzey2010-12-16
* * Kernel/Term:Gravatar regisgia2010-12-01
* * Kernel/TermGravatar regisgia2010-12-01
* * Kernel/TermGravatar regisgia2010-12-01
* Minor fixes from Gregory Malecha. A typo fixed and a better (located) Gravatar msozeau2010-11-15
* Correction bug 2427Gravatar soubiran2010-11-03
* Remove suspiciously named "implicit" stuff from TermGravatar glondu2010-11-03
* In Univ, unify order_request and constraint_typeGravatar glondu2010-11-03
* More generic Univ.dump_universesGravatar glondu2010-11-02
* Reintroduce kind_of_type (used by Presburger contrib)Gravatar glondu2010-10-05
* Forgotten lifts in eta-expansionGravatar glondu2010-10-04
* Fixing printing of module_path names (was using a debuggingGravatar herbelin2010-10-03
* Remove kind_of_type, kind_of_term2 (dead code)Gravatar glondu2010-09-28
* Partial review of removed dead code (r13460)Gravatar herbelin2010-09-24