index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
Commit message (
Expand
)
Author
Age
*
Printing bugs with match patterns:
herbelin
2012-01-27
*
Fix for Program Instance not separately checking the resolution of evars of t...
msozeau
2012-01-23
*
Inductiveops.nb_*{,_env} cleaning
pboutill
2012-01-16
*
Type inference unification: fixed a 8.4 bug in the presence of unification
herbelin
2012-01-04
*
Granted legitimate wish #2607 (not exposing crude fixpoint body of
herbelin
2011-12-18
*
Continuing 14812 and 14813 (use type information to reduce the
herbelin
2011-12-18
*
Added a flag to control the use of typing when instantiating applied
herbelin
2011-12-17
*
Added ability to take the type of applied metas into account when
herbelin
2011-12-17
*
Reorganizing Unification.unify_0 so as to more easily share code
herbelin
2011-12-17
*
A pass on warning printings. Made systematic the use of msg_warning so
herbelin
2011-12-17
*
Introducing a notion of evar candidates to be used when an evar is
herbelin
2011-12-16
*
Fixing a bug of commit r13310 (activating coercions only when module
herbelin
2011-12-07
*
Backtrack on synchronizing universe counter with reset
herbelin
2011-12-06
*
Registering universe and meta/evar counters as summaries so as to
herbelin
2011-12-05
*
Yet another fix about alias in testing if pattern unification applies.
herbelin
2011-12-05
*
Fixed a small regression in pattern-matching compilation introduced in
herbelin
2011-12-04
*
Discarding let-ins from the instances of the evars in the
herbelin
2011-12-04
*
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-28
*
Fixed a bug in postprocessing dependencies in pattern-matching compilation
herbelin
2011-11-26
*
avoid relying on weak invariant in cbv.ml
bgregoir
2011-11-25
*
Added a DEPRECATED flag in declaration of options. For now only two options a...
ppedrot
2011-11-24
*
Adds a pair of function in Evar_util to gather dependent evars in an
aspiwack
2011-11-23
*
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-21
*
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-18
*
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-17
*
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-16
*
Refined second_order_matching so that a constraint on which
herbelin
2011-11-08
[next]