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
*
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
*
avoid (Int.equal (cmp ...) 0) when a boolean equality exists
letouzey
2013-02-19
*
Dir_path --> DirPath
letouzey
2013-02-19
*
Classops : avoid some use of Gmap
letouzey
2013-02-19
*
Removing Exc_located and using the new exception enrichement
ppedrot
2013-02-18
*
use List.rev_map whenever possible
letouzey
2013-02-18
*
Minor code cleanups, especially take advantage of Dir_path.is_empty
letouzey
2013-02-18
*
Displaying environment and unfolding aliases in "cannot_unify"
herbelin
2013-02-17
*
A more informative message when the elimination predicate for
herbelin
2013-02-17
*
Locating errors from consider_remaining_unif_problems if possible
herbelin
2013-02-17
*
Added propagation of evars unification failure reasons for better
herbelin
2013-02-17
*
Splitted Evarutil in two files
ppedrot
2013-02-10
*
Moved code from Pretype_error to Evarutil
ppedrot
2013-02-10
*
Revert "Ordered evars by level of dependency in the merging phase of unificat...
herbelin
2013-02-05
*
Fixed bug #2981 (anomaly NotASort in Retyping due to collision between
herbelin
2013-02-05
*
Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_env
herbelin
2013-01-29
*
Actually adding backtrace handling.
ppedrot
2013-01-28
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Fixing one part of #2830 (anomaly "defined twice" due to nested calls to
herbelin
2013-01-28
*
Added backtrace information to anomalies
ppedrot
2013-01-28
*
Ordered evars by level of dependency in the merging phase of unification
herbelin
2013-01-27
*
Improving formatting of output of "Test table".
herbelin
2013-01-27
*
Reductionops: whd_state_gen can take and answers a cst_stack too
pboutill
2013-01-24
*
New implementation of the conversion test, using normalization by evaluation to
mdenes
2013-01-22
*
- Fix evarconv so that we have complete eta-conversion:
msozeau
2013-01-22
[next]