| Age | Commit message (Expand) | Author |
|---|
| 2013-11-02 | Getting rid of Goal.here, and all the related exceptions and combinators. | aspiwack |
| 2013-11-02 | Uses Proofview.tclEXTEND more sparingly. | aspiwack |
| 2013-11-02 | Makes the new Proofview.tactic the basic type of Ltac. | aspiwack |
| 2013-11-02 | Closure: fix an issue with r16959 spotted by Matthieu | letouzey |
| 2013-10-31 | Mod_subst.update_delta_resolver : avoid loosing Inline(_,Some _) | letouzey |
| 2013-10-31 | Fixing Kerpair.hash. Since the beginning, it dit not respect the type | ppedrot |
| 2013-10-31 | Future: better doc + restore ~pure optimization | gareuselesinge |
| 2013-10-31 | CoqIDE: scroll to the right position if there is an interp error | gareuselesinge |
| 2013-10-31 | Conv_orable made functional and part of pre_env | gareuselesinge |
| 2013-10-31 | Efficient filtered functions in Evd. We test that a filter is actually | ppedrot |
| 2013-10-31 | Avoiding useless allocations in Closure. | ppedrot |
| 2013-10-30 | Various optimizations of Evd.meta_* functions. | ppedrot |
| 2013-10-30 | More efficient implementation of [Evd.retract_coercible_metas]. | ppedrot |
| 2013-10-29 | Optimization in unification: when checking that the head of a term is an | ppedrot |
| 2013-10-29 | Useless array-to-list casts in Unification. | ppedrot |
| 2013-10-29 | Do not generate useless argument arrays in whd_* functions. | ppedrot |
| 2013-10-29 | Prevent [Evarutil.whd_head_evar] from uselessly reallocating arrays. | ppedrot |
| 2013-10-29 | [Reductionops.append_stack_app]: do not allocate a useless array. | ppedrot |
| 2013-10-29 | Revert the two last commits. My bad, I messed up git-svn commands... | ppedrot |
| 2013-10-29 | Profile only when CAMLRUNPARAM is set. | ppedrot |
| 2013-10-29 | Printing heap on every processed sentence. | ppedrot |
| 2013-10-29 | Sharing identity evar filters. | ppedrot |
| 2013-10-29 | Allocation-friendly version of [Pre_env.push_named]. | ppedrot |
| 2013-10-29 | Optimizing universes: tail-rec, allocation friendly [compare_leq]. | ppedrot |
| 2013-10-29 | - install evar printer for debugging | msozeau |
| 2013-10-28 | Native compiler: library compilation errors are now non fatal. | mdenes |
| 2013-10-28 | Evar leak in "absurd" tactic. | ppedrot |
| 2013-10-28 | Removing Evd.undefined_evars. | ppedrot |
| 2013-10-28 | Useless array to list conversions in proof/logic.ml. | ppedrot |
| 2013-10-27 | Removing useless filter allocation in evar construction. | ppedrot |
| 2013-10-27 | Abstracting evar filter away. The API is not perfect, but better than nothing. | ppedrot |
| 2013-10-27 | More sharing in Constr.map_with_binders. | ppedrot |
| 2013-10-27 | Closure optimizations. | ppedrot |
| 2013-10-24 | More monomorphic List.mem + List.assoc + ... | letouzey |
| 2013-10-24 | inductive.ml : get rid of some obvious (Lazy.force (lazy t)) | letouzey |
| 2013-10-24 | Rtree : cleanup of the comparing code | letouzey |
| 2013-10-24 | Specializing hash functions for widely used types. | ppedrot |
| 2013-10-24 | Restore my version of notation_ops.ml now that List.remove_assoc_f is fixed | letouzey |
| 2013-10-24 | Fix the semantic of the new List.remove_assoc_f | letouzey |
| 2013-10-24 | Oups, repair the compilation (micromega + Morphism_prop) | letouzey |
| 2013-10-24 | Ephemeron: add a function to run a collection cycle | gareuselesinge |
| 2013-10-24 | CoqIDE: fix coloring bug when jumping back to the first phrase | gareuselesinge |
| 2013-10-24 | Get rid of polymorphic comparison in "plugins/btauto/refl_btauto.ml". | xclerc |
| 2013-10-24 | Get rid of polymorphic equality in "checker/subtyping.ml". | xclerc |
| 2013-10-24 | Turn many List.assoc into List.assoc_f | letouzey |
| 2013-10-23 | cList: a few alternative to hashtbl-based uniquize, distinct, subset | letouzey |
| 2013-10-23 | CList.factorize_left with a parametric equality | letouzey |
| 2013-10-23 | CList.prefix_of and CList.drop_prefix with a parametric equality | letouzey |
| 2013-10-23 | cList.index is now cList.index_f, same for index0 | letouzey |
| 2013-10-23 | cList: set-as-list functions are now with an explicit comparison | letouzey |
