index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
cases.ml
Commit message (
Expand
)
Author
Age
...
*
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
*
Fixing new bug introduced in r14665 when fixing bug #1834.
herbelin
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
*
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-25
*
It happens that the type inference algorithm (pretyping) did not check
herbelin
2011-10-05
*
Two bugs in pattern-matching compilation:
herbelin
2011-08-08
*
Cases: generic equality on constr replaced by destructors
puech
2011-07-29
*
Fix inductive_template building ill-typed evars, and update test-suite scripts
msozeau
2011-03-13
*
Tentative to make unification check types at every instanciation of an
msozeau
2011-03-11
*
More {raw => glob} changes for consistency
glondu
2010-12-24
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-23
*
Fixing bug #2454: inversion predicate strategy for inferring the type
herbelin
2010-12-19
*
Fixing the Not_found error in bug #2404 + dead code removal in cases.ml
herbelin
2010-10-06
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Extension of the recursive notations mechanism
herbelin
2010-07-22
*
Made tclABSTRACT normalize evars before saying it does not support
herbelin
2010-06-29
*
Improved the inference of the return predicate in dependent pattern-matching.
herbelin
2010-06-12
*
Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).
herbelin
2010-06-11
*
Fixed two bugs in pattern-matching compilation
herbelin
2010-06-10
*
Fix bug 2307
pboutill
2010-05-20
*
Add (almost) compatibility with camlp4, without breaking support for camlp5
letouzey
2010-05-19
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Fixing bug #2193: computation of dependencies in the "match" return
herbelin
2009-12-30
*
Added support for definition of fixpoints using tactics.
herbelin
2009-11-27
*
Promote evar_defs to evar_map (in Evd)
glondu
2009-11-11
*
A bit of cleaning around name generation + creation of dedicated file namegen.ml
herbelin
2009-11-09
*
Improved the treatment of Local/Global options (noneffective Local on
herbelin
2009-10-25
*
This big commit addresses two problems:
soubiran
2009-10-21
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Ensures that let-in's in arities of inductive types work well. Maybe not
herbelin
2009-08-11
*
Jolification : tentative de supprimer les "( evd)" et associƩs qui
aspiwack
2009-07-07
*
Improve return predicate inference by making the return type dependent
msozeau
2009-06-28
*
Fixing bug #2106 ("match" compilation with multi-dependent constructor).
herbelin
2009-06-06
*
Some dead code removal + cleanups
letouzey
2009-04-08
[prev]
[next]