coq - The formal proof system

Age	Commit message (Expand)	Author
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
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-08	catch failures of pr_vernac to make -time failsafe	gareuselesinge
2013-03-08	Use with_state_protection in pr_module_vardecls	gareuselesinge
2013-03-05	More monomorphization.	ppedrot
2013-03-05	Missing primitive in CArray	ppedrot
2013-02-28	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-27	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-26	kernel/declarations becomes a pure mli	letouzey
2013-02-26	Names: shortcuts for building {kn, constant, mind} with empty sections	letouzey
2013-02-26	Names: Modularize constant and mutual_inductive	letouzey
2013-02-26	Mod_subst: misc reformulations	letouzey
2013-02-25	cbn friendly VectorDef	pboutill
2013-02-25	Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo...	pboutill
2013-02-25	CoqIDE: Add TAB key to autocomplete	ppedrot
2013-02-24	Fixing bug #2466	ppedrot
2013-02-24	New -no-native-compiler flag for configure, globally disabling the native	mdenes
2013-02-24	Reduced the noise level when dynlinking in bytecode mode or when	mdenes
2013-02-22	Tentative heuristic fix to handle lexer failures from CoqIDE when	ppedrot
2013-02-22	Cosmetic changes to CoqIDE finder widget.	ppedrot
2013-02-21	Names: con_modpath and con_label access back the user kn part	letouzey
2013-02-21	Added missing documentation of Set Printing Existential Instances.	herbelin
2013-02-21	A slightly more efficient test of well-typedness of restriction of	herbelin
2013-02-21	Added Evarsolve to the list of modules to open for debugging.	herbelin
2013-02-20	Fixing an annoying bug in CoqIDE which causes the very first line	ppedrot
2013-02-20	Fixing #2763	ppedrot