index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
pretyping
/
cases.ml
Age
Commit message (
Expand
)
Author
2012-01-16
Inductiveops.nb_*{,_env} cleaning
pboutill
2011-12-16
Introducing a notion of evar candidates to be used when an evar is
herbelin
2011-12-04
Fixed a small regression in pattern-matching compilation introduced in
herbelin
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-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-17
Fixing new bug introduced in r14665 when fixing bug #1834.
herbelin
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-10-25
Fixing use of type constraint for refining the "return" clause of "match".
herbelin
2011-10-25
New strategy to infer return predicate of match construct when
herbelin
2011-10-05
It happens that the type inference algorithm (pretyping) did not check
herbelin
2011-08-08
Two bugs in pattern-matching compilation:
herbelin
2011-07-29
Cases: generic equality on constr replaced by destructors
puech
2011-03-13
Fix inductive_template building ill-typed evars, and update test-suite scripts
msozeau
2011-03-11
Tentative to make unification check types at every instanciation of an
msozeau
2010-12-24
More {raw => glob} changes for consistency
glondu
2010-12-23
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-19
Fixing bug #2454: inversion predicate strategy for inferring the type
herbelin
2010-10-06
Fixing the Not_found error in bug #2404 + dead code removal in cases.ml
herbelin
2010-09-24
Some dead code removal, thanks to Oug analyzer
letouzey
2010-07-24
Updated all headers for 8.3 and trunk
herbelin
2010-07-22
Extension of the recursive notations mechanism
herbelin
2010-06-29
Made tclABSTRACT normalize evars before saying it does not support
herbelin
2010-06-12
Improved the inference of the return predicate in dependent pattern-matching.
herbelin
2010-06-11
Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).
herbelin
2010-06-10
Fixed two bugs in pattern-matching compilation
herbelin
2010-05-20
Fix bug 2307
pboutill
2010-05-19
Add (almost) compatibility with camlp4, without breaking support for camlp5
letouzey
2010-04-29
Remove the svn-specific $Id$ annotations
letouzey
2009-12-30
Fixing bug #2193: computation of dependencies in the "match" return
herbelin
[next]