coq - The formal proof system

Age	Commit message (Expand)	Author
2013-03-18	Fix for bug #3004 (thanks Hugo!)	letouzey
2013-03-18	Extraction AccessOpaque is now activated again by default (#2952)	letouzey
2013-03-18	Making local variable warning verbose by default.	ppedrot
2013-03-17	Ppvernac: no globalization for printing ltac definitions	letouzey
2013-03-17	Fix some camlp5 quotations , restoring compatibility with camlp5 5.x	letouzey
2013-03-17	Checker: simplify a bit its exception handler	letouzey
2013-03-17	Avoid a few overzealous "when Errors.noncritical"	letouzey
2013-03-17	Retyping.get_type_of: a lax version raising no anomalies	letouzey
2013-03-16	another Errors.push in a exception reraise	letouzey
2013-03-15	Extract_env : correct exceptions mentionned in a try ... with	letouzey
2013-03-14	Embedded exns in LtacLocated and EvaluatedError satisfy Errors.noncritical	letouzey
2013-03-14	Cerrors: get rid of some FIXME	letouzey
2013-03-14	Typo in an error message	letouzey
2013-03-14	Use Pp.msg instead of Pp.pp in -beautify (loss of text otherwise)	letouzey
2013-03-14	Pptactic.pr_raw_tactic is now without env argument	letouzey
2013-03-13	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-12	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-11	Allowing (Co)Fixpoint to be defined local and Let-style.	ppedrot