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
...
*
A uniformization step around understand_* and interp_* functions.
herbelin
2013-05-09
*
A few comments in evarconv.mli.
herbelin
2013-05-09
*
Uniformization: isevars -> evdref/sigma/evd
herbelin
2013-05-09
*
Uniformizing the [if_warn] flag used for warning printing and put
ppedrot
2013-05-08
*
Protection against "Bad recursive type" in w_unify0 (bug #3036).
herbelin
2013-05-08
*
Fixing ocamldoc compilation.
ppedrot
2013-05-06
*
Small cleaning of Evd interface.
ppedrot
2013-05-06
*
States: frozen states can hold closures
gareuselesinge
2013-05-06
*
Hack to solve a "Bad recursive type" anomaly.
herbelin
2013-05-05
*
Removing a redundant function from Evd.
ppedrot
2013-05-03
*
Fix wrong computation of dependency signature in cases raising an uncaught ex...
msozeau
2013-04-30
*
Merging Context and Sign.
ppedrot
2013-04-29
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
code simplifications concerning Summary
letouzey
2013-04-22
*
Finer fix for bug 3017, mark unresolvability only of goals that are
msozeau
2013-04-18
*
Fix #3001 (rename arg of global cst inside section)
gareuselesinge
2013-04-18
*
Matching patterns: fixed allow_partial_app which was not working on
herbelin
2013-04-17
*
Fix of r16257 in r16205 for "errors raised by check_evar_instance were
herbelin
2013-04-17
*
Like in r16346, do not filter local definitions (here in the
herbelin
2013-04-17
*
Fix for bug #3017: wrong handling of the unresolvability status
msozeau
2013-04-03
*
Continuation of r16346 on filtering local definitions. Refined
herbelin
2013-03-30
*
Native compiler: timing info for reification in debug mode.
mdenes
2013-03-25
*
Fix bug #2989: make unification.ml able to deal with canonical structure in a...
pboutill
2013-03-25
*
Comments in mli
pboutill
2013-03-25
*
Minor code cleaning in CArray / CList.
ppedrot
2013-03-23
*
Fix bug# 2994, 2971 about better error messages.
msozeau
2013-03-22
*
Fixing unfolding of local definitions during unification that appeared
herbelin
2013-03-21
*
Cosmetic code contraction in evarsolve.ml + test sur unification avec let-in.
herbelin
2013-03-21
*
Using hnf instead of "intro H" for forcing reduction to a product.
herbelin
2013-03-21
*
Fixing an old pecularity of "red": head betaiota redexes are now
herbelin
2013-03-21
*
Check a list length before doing a List.chop (fix #3000)
letouzey
2013-03-20
*
Fix for bug #3004 (thanks Hugo!)
letouzey
2013-03-18
*
Avoid a few overzealous "when Errors.noncritical"
letouzey
2013-03-17
*
Retyping.get_type_of: a lax version raising no anomalies
letouzey
2013-03-17
*
Typo in an error message
letouzey
2013-03-14
*
Restrict (try...with...) to avoid catching critical exn (part 12)
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 7)
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 5)
letouzey
2013-03-13
*
A version of Univ.check_eq with no anomaly for Evd.set_eq_sort
letouzey
2013-03-12
*
Term.dest* functions now raise specific DestKO exn instead of Invalid_argument
letouzey
2013-03-12
*
invalid_arg instead of raise (Invalid_argement ...)
letouzey
2013-03-12
*
Allowing different types of, not to be mixed, generic Stores through
ppedrot
2013-03-12
*
Added a Local Definition vernacular command. This type of definition
ppedrot
2013-03-11
*
More monomorphization.
ppedrot
2013-03-05
*
compare_stack_shape before ise_stack2 in evar_conv
pboutill
2013-02-28
*
Repairing r16205: errors raised by check_evar_instance were no longer
herbelin
2013-02-28
*
More informative error when a global reference is used in a context of
herbelin
2013-02-28
*
kernel/declarations becomes a pure mli
letouzey
2013-02-26
*
Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo...
pboutill
2013-02-25
*
A slightly more efficient test of well-typedness of restriction of
herbelin
2013-02-21
[prev]
[next]