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
*
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
*
Fixed parsing of -no-native-compiler flag.
mdenes
2013-01-24
*
New implementation of the conversion test, using normalization by evaluation to
mdenes
2013-01-22
*
Array.create is deprecated
pboutill
2012-12-19
*
Modulification of name
ppedrot
2012-12-18
*
Modulification of Label
ppedrot
2012-12-18
*
Ide_slave: do not prepare debug messages in non-debug mode
letouzey
2012-12-17
*
Modulification of dir_path
ppedrot
2012-12-14
*
Modulification of identifier
ppedrot
2012-12-14
*
Moved Stringset and Stringmap to String namespace.
ppedrot
2012-12-14
*
Moved Intset and Intmap to Int namespace.
ppedrot
2012-12-14
*
Implemented a full-fledged equality on [constr_expr]. By the way,
ppedrot
2012-12-14
*
Using library string functions.
ppedrot
2012-12-13
*
Renamed Option.Misc.compare to the more uniform Option.equal.
ppedrot
2012-12-13
*
Ensure that a function declared with a label is used with it
letouzey
2012-12-08
*
Finish patch for Hint Resolve, stopping to generate new constant names for
msozeau
2012-12-08
*
Restoring flush of Welcome message lost in r15148
herbelin
2012-12-06
*
Removed Compat.Exc_located outside of compat.ml4, as a consequence of
herbelin
2012-12-04
*
Low-level hack to get some more informative message from dynamic loading errors.
herbelin
2012-12-04
*
Revised the strategy for automatic insertion of spaces when printing
herbelin
2012-12-04
[next]