aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Modules and ppvernac, sequel of Enrico's commit 16261Gravatar letouzey2013-03-13
* Declaremods: a few syntactic improvementsGravatar letouzey2013-03-13
* Made the backtrace type opaqueGravatar ppedrot2013-03-13
* Fix compilation of coqchk (broken by commit 16268), bis repetitaGravatar letouzey2013-03-13
* Fix compilation of coqchk (broken by commit 16268)Gravatar letouzey2013-03-13
* Toplevel: improved commentsGravatar letouzey2013-03-13
* Vernac+Toplevel: get rid of Error_in_fileGravatar letouzey2013-03-13
* Vernac+Toplevel: get rid of DuringVernacInterpGravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 15)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 14)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 13)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 12)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 12)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 11)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 10)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 9)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 8)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 7)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 6)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 5)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 4)Gravatar letouzey2013-03-12
* Implicit_quantifiers.is_freevar: cleaner, no more try...with _ ->...Gravatar letouzey2013-03-12
* Restrict (try...with...) to avoid catching critical exn (part 3)Gravatar letouzey2013-03-12
* Restrict (try...with...) to avoid catching critical exn (part 2)Gravatar letouzey2013-03-12
* Restrict (try...with...) to avoid catching critical exn (part 1)Gravatar letouzey2013-03-12
* Hipattern : consider jmeq only when Logic.JMeq is loadedGravatar letouzey2013-03-12
* A version of Univ.check_eq with no anomaly for Evd.set_eq_sortGravatar letouzey2013-03-12
* Equality: avoid an anomaly about inj_pair2_eq_decGravatar letouzey2013-03-12
* Recdef: an anomaly isn't so anomalous, occurs in 1618.vGravatar letouzey2013-03-12
* Term.dest* functions now raise specific DestKO exn instead of Invalid_argumentGravatar letouzey2013-03-12
* invalid_arg instead of raise (Invalid_argement ...)Gravatar letouzey2013-03-12
* New function Errors.noncritical for restricting try ... with ...Gravatar letouzey2013-03-12
* Updated Exninfo to the new Store type.Gravatar ppedrot2013-03-12
* Allowing different types of, not to be mixed, generic Stores throughGravatar ppedrot2013-03-12
* Allowing (Co)Fixpoint to be defined local and Let-style.Gravatar ppedrot2013-03-11
* Obligations generated by Program are now local.Gravatar ppedrot2013-03-11
* Documentation of the "Local Definition" command.Gravatar ppedrot2013-03-11
* Added a Local Definition vernacular command. This type of definitionGravatar ppedrot2013-03-11
* catch failures of pr_vernac to make -time failsafeGravatar gareuselesinge2013-03-08
* Use with_state_protection in pr_module_vardeclsGravatar gareuselesinge2013-03-08
* More monomorphization.Gravatar ppedrot2013-03-05
* Missing primitive in CArrayGravatar ppedrot2013-03-05
* compare_stack_shape before ise_stack2 in evar_convGravatar pboutill2013-02-28
* Repairing r16205: errors raised by check_evar_instance were no longerGravatar herbelin2013-02-28
* More informative error when a global reference is used in a context ofGravatar herbelin2013-02-28
* Coqlib: minor simplificationsGravatar letouzey2013-02-27
* Update debug code according to reorganization into modules.Gravatar msozeau2013-02-27
* Minor cleanup around Term_typingGravatar letouzey2013-02-27
* remove a warning after Drop about print_hint_dbGravatar letouzey2013-02-27
* Adapt dev/base_include to new DeclarationsGravatar letouzey2013-02-27