index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Cleanup of comments.
aspiwack
2013-11-02
*
Plug back the declarative mode.
aspiwack
2013-11-02
*
Small change to the IO monad interface: [val ref : 'a -> 'a ref t]
aspiwack
2013-11-02
*
A whole new implemenation of the refine tactic.
aspiwack
2013-11-02
*
A newly introduced variable inside a named context is no longer α-renamed.
aspiwack
2013-11-02
*
Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.
aspiwack
2013-11-02
*
Bases tactics on an IO monad.
aspiwack
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-11-02
*
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-31
*
Various optimizations of Evd.meta_* functions.
ppedrot
2013-10-30
*
More efficient implementation of [Evd.retract_coercible_metas].
ppedrot
2013-10-30
*
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-29
*
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-28
*
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-27
*
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
[next]