index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
pretyping
Age
Commit message (
Expand
)
Author
2011-11-28
Finally used typing to decide whether an alias needs to be expanded or
herbelin
2011-11-28
Fixing dependencies postprocessing bug in pattern-matching compilation.
herbelin
2011-11-26
Fixed a bug in postprocessing dependencies in pattern-matching compilation
herbelin
2011-11-25
avoid relying on weak invariant in cbv.ml
bgregoir
2011-11-24
Added a DEPRECATED flag in declaration of options. For now only two options a...
ppedrot
2011-11-23
Adds a pair of function in Evar_util to gather dependent evars in an
aspiwack
2011-11-21
Renamig support added to "Arguments"
gareuselesinge
2011-11-21
Configurable simpl tactic
gareuselesinge
2011-11-21
Extend the computation of dependencies in pattern-matching compilation
herbelin
2011-11-21
Add matching on non-inductive types in building an inversion problem
herbelin
2011-11-21
Old naming bug in pattern-matching compilation: names in the
herbelin
2011-11-21
Inlining let-in (i.e. trace of aliases) in extract_predicate for what
herbelin
2011-11-21
In pattern-matching compilation, now taking into account the dependencies
herbelin
2011-11-21
Optimizing the compilation of unused aliases in pattern-matching.
herbelin
2011-11-21
Simplifying history management in pattern-matching compilation.
herbelin
2011-11-21
Fixing postprocessing bugs in pattern-matching compilation.
herbelin
2011-11-21
Removing stuff about alias dependencies now become useless.
herbelin
2011-11-21
Changed the way to detect if an "as" patterns is expanded or not. The
herbelin
2011-11-21
Dead code + refreshing some comments in cases.ml.
herbelin
2011-11-18
Restore backward compatibility. ":>" declares subinstances in Class declarati...
msozeau
2011-11-18
Fix for subclasses implementation, allowing to register generalized classes s...
msozeau
2011-11-17
Fixing new bug introduced in r14665 when fixing bug #1834.
herbelin
2011-11-17
Merge subinstances branch by me and Tom Prince.
msozeau
2011-11-16
Adding postprocessing to remove "commutative cuts" expansions in
herbelin
2011-11-16
Changed the way find_dependencies_signature is working so that it
herbelin
2011-11-16
De Bruijn indices bug in pattern matching compilation in the presence
herbelin
2011-11-16
Old generalization bug in pattern-matching: names were considered the
herbelin
2011-11-16
Fixing bug #1834 (de Bruijn indices bug in pattern-matching compilation).
herbelin
2011-11-16
Old typing bug in pattern-matching compilation (apparently w/o
herbelin
2011-11-16
Specialization of tomatch in pattern-matching compilation was done too
herbelin
2011-11-16
A bit of documentation around cases.ml + ML modules uselessly open
herbelin
2011-11-16
Fixing dependencies lifting bug in pattern-matching compilation
herbelin
2011-11-08
Refined second_order_matching so that a constraint on which
herbelin
2011-11-08
optimization: memoization for is_open_canonical_projection
gareuselesinge
2011-11-08
Improved check is_open_canonical_projection
gareuselesinge
2011-11-07
Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructors
letouzey
2011-11-06
Fixing incorrect change to pattern-unification over Meta's introduced
herbelin
2011-11-02
Add type annotations around all calls to Libobject.declare_object
letouzey
2011-10-28
Remove dynamic stuff from constr_expr and glob_constr
glondu
2011-10-26
Deactivating second-order pattern-matching in evarconv for 8.4.
herbelin
2011-10-26
When checking for emptiness, use Foo.is_empty instead of (=) Foo.empty
letouzey
2011-10-25
Fixing use of type constraint for refining the "return" clause of "match".
herbelin
2011-10-25
Continuing r14585 (ill-typed restriction bug).
herbelin
2011-10-25
Continuing r1492 (useless changes were inadvertantly committed)
herbelin
2011-10-25
New strategy to infer return predicate of match construct when
herbelin
2011-10-25
Still more unification in typing.ml
herbelin
2011-10-24
More unification in type_of and addition of e_type_of to get the new
herbelin
2011-10-24
Fixing another bug revealing ill-typed use of evar restriction.
herbelin
2011-10-24
Fixing instance/filter mismatch in materialize_evar + documentation.
herbelin
2011-10-22
Fail if some conv pbs remain after consider_remaining_unif_problems.
herbelin
[next]