index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
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
*
Robust display of NotConvertibleTypeField errors (fix #3008, #2995)
letouzey
2013-03-21
*
Typo dans message d'erreur (obligations).
herbelin
2013-03-21
*
Add type information in error message when a constructor is not fully
herbelin
2013-03-21
*
Check unexpected "Local" keyword in cmd before opening a proof (fix #2975)
letouzey
2013-03-21
*
Removing the module Libtypes and unifying the Search[Pattern|Rewrite]?
ppedrot
2013-03-19
*
Making local variable warning verbose by default.
ppedrot
2013-03-18
*
Avoid a few overzealous "when Errors.noncritical"
letouzey
2013-03-17
*
Embedded exns in LtacLocated and EvaluatedError satisfy Errors.noncritical
letouzey
2013-03-14
*
Cerrors: get rid of some FIXME
letouzey
2013-03-14
*
Use Pp.msg instead of Pp.pp in -beautify (loss of text otherwise)
letouzey
2013-03-14
*
Modules and ppvernac, sequel of Enrico's commit 16261
letouzey
2013-03-13
*
Toplevel: improved comments
letouzey
2013-03-13
*
Vernac+Toplevel: get rid of Error_in_file
letouzey
2013-03-13
*
Vernac+Toplevel: get rid of DuringVernacInterp
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 14)
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 13)
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 10)
letouzey
2013-03-13
*
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
*
Allowing (Co)Fixpoint to be defined local and Let-style.
ppedrot
2013-03-11
*
Obligations generated by Program are now local.
ppedrot
2013-03-11
*
Added a Local Definition vernacular command. This type of definition
ppedrot
2013-03-11
*
catch failures of pr_vernac to make -time failsafe
gareuselesinge
2013-03-08
*
More monomorphization.
ppedrot
2013-03-05
*
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
*
Update debug code according to reorganization into modules.
msozeau
2013-02-27
*
kernel/declarations becomes a pure mli
letouzey
2013-02-26
*
Fixing bug #2466
ppedrot
2013-02-24
*
Corrects bug #2959 (error during Qed leads to assertion failure).
aspiwack
2013-02-20
*
avoid (Int.equal (cmp ...) 0) when a boolean equality exists
letouzey
2013-02-19
*
Dir_path --> DirPath
letouzey
2013-02-19
*
Names: revised representation of constants and mutual_inductive
letouzey
2013-02-19
*
Removing Exc_located and using the new exception enrichement
ppedrot
2013-02-18
*
Updating the backtrace handling mechanism to accomodate the new
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
*
Added propagation of evars unification failure reasons for better
herbelin
2013-02-17
*
Revised the Ltac trace mechanism so that trace breaking due to
herbelin
2013-02-17
*
Useless use of hooks in VernacDefinition. In addition, this was
ppedrot
2013-02-10
*
Moved code from Pretype_error to Evarutil
ppedrot
2013-02-10
*
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
*
Added backtrace information to anomalies
ppedrot
2013-01-28
*
Fixed bug #2967 (some missing check on ill-formed recursive notation strings).
herbelin
2013-01-27
[next]