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
*
Fixing a source of evars leak, revealed by contrib QuicksortComplexity
herbelin
2013-05-11
*
Uniformization: isevars -> evdref/sigma/evd
herbelin
2013-05-09
*
Fix wrong computation of dependency signature in cases raising an uncaught ex...
msozeau
2013-04-30
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Restrict (try...with...) to avoid catching critical exn (part 12)
letouzey
2013-03-13
*
invalid_arg instead of raise (Invalid_argement ...)
letouzey
2013-03-12
*
Removing Exc_located and using the new exception enrichement
ppedrot
2013-02-18
*
use List.rev_map whenever possible
letouzey
2013-02-18
*
Splitted Evarutil in two files
ppedrot
2013-02-10
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Array.create is deprecated
pboutill
2012-12-19
*
Modulification of name
ppedrot
2012-12-18
*
Fixed a bug in the algorithm trying to elaborate a "match" return predicate.
herbelin
2012-12-17
*
Modulification of identifier
ppedrot
2012-12-14
*
Moved Intset and Intmap to Int namespace.
ppedrot
2012-12-14
*
Monomorphization (pretyping)
ppedrot
2012-11-22
*
Monomorphized a lot of equalities over OCaml integers, thanks to
ppedrot
2012-11-08
*
Remove some more "open" and dead code thanks to OCaml4 warnings
letouzey
2012-10-02
*
More cleaning on Utils and CList. Some parts of the code being
ppedrot
2012-09-17
*
Some documentation and cleaning of CList and Util interfaces.
ppedrot
2012-09-15
*
As r15801: putting everything from Util.array_* to CArray.*.
ppedrot
2012-09-14
*
Moving Utils.list_* to a proper CList module, which includes stdlib
ppedrot
2012-09-14
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
The new ocaml compiler (4.00) has a lot of very cool warnings,
regisgia
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
Glob_term now mli-only, operations now in Glob_ops
letouzey
2012-05-29
*
Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd
letouzey
2012-05-29
*
Impossible branches inference fixup (bug 2761)
pboutill
2012-05-11
*
Fix bugs related to Program integration.
msozeau
2012-03-19
*
Revise API of understand_ltac to be parameterized by a flag for resolution of...
msozeau
2012-03-14
*
Merge fixes
msozeau
2012-03-14
*
Everything compiles again.
msozeau
2012-03-14
*
Second step of integration of Program:
msozeau
2012-03-14
*
Remove support for "abstract typing constraints" that requires unicity of sol...
msozeau
2012-03-14
*
A bit of cleaning: unifying push_rels and push_rel_context.
herbelin
2012-03-13
*
Glob_term.predicate_pattern: No number of parameters with letins.
pboutill
2012-03-02
*
Noise for nothing
pboutill
2012-03-02
*
Inductiveops.nb_*{,_env} cleaning
pboutill
2012-01-16
*
Introducing a notion of evar candidates to be used when an evar is
herbelin
2011-12-16
*
Fixed a small regression in pattern-matching compilation introduced in
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
*
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
[next]