index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Modules and ppvernac, sequel of Enrico's commit 16261
letouzey
2013-03-13
*
Declaremods: a few syntactic improvements
letouzey
2013-03-13
*
Made the backtrace type opaque
ppedrot
2013-03-13
*
Fix compilation of coqchk (broken by commit 16268), bis repetita
letouzey
2013-03-13
*
Fix compilation of coqchk (broken by commit 16268)
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 15)
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 12)
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 12)
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 11)
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 10)
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 9)
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 8)
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 6)
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 5)
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 4)
letouzey
2013-03-12
*
Implicit_quantifiers.is_freevar: cleaner, no more try...with _ ->...
letouzey
2013-03-12
*
Restrict (try...with...) to avoid catching critical exn (part 3)
letouzey
2013-03-12
*
Restrict (try...with...) to avoid catching critical exn (part 2)
letouzey
2013-03-12
*
Restrict (try...with...) to avoid catching critical exn (part 1)
letouzey
2013-03-12
*
Hipattern : consider jmeq only when Logic.JMeq is loaded
letouzey
2013-03-12
*
A version of Univ.check_eq with no anomaly for Evd.set_eq_sort
letouzey
2013-03-12
*
Equality: avoid an anomaly about inj_pair2_eq_dec
letouzey
2013-03-12
*
Recdef: an anomaly isn't so anomalous, occurs in 1618.v
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
*
New function Errors.noncritical for restricting try ... with ...
letouzey
2013-03-12
*
Updated Exninfo to the new Store type.
ppedrot
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
*
Documentation of the "Local Definition" command.
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
*
Use with_state_protection in pr_module_vardecls
gareuselesinge
2013-03-08
*
More monomorphization.
ppedrot
2013-03-05
*
Missing primitive in CArray
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
*
Coqlib: minor simplifications
letouzey
2013-02-27
*
Update debug code according to reorganization into modules.
msozeau
2013-02-27
*
Minor cleanup around Term_typing
letouzey
2013-02-27
*
remove a warning after Drop about print_hint_db
letouzey
2013-02-27
*
Adapt dev/base_include to new Declarations
letouzey
2013-02-27
[next]