aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2013-04-25raise UnsafeSuccess -> feedback AddedAxiomgareuselesinge
2013-04-25Coqide: new feedback mechanism for structured contentgareuselesinge
2013-04-23Fix issues with "Reset Initial" in scripts given to coqtop -lletouzey
2013-04-23minor cleanup in coqtop.mlletouzey
2013-04-23coqtop -compile: avoid with_heavy_rollback when non-interactiveletouzey
2013-04-23Coqtop -compile : avoid saving init state when compiling just one fileletouzey
2013-04-23Remove deprecated option -no-hash-consing (currently doing nothing)letouzey
2013-04-22code simplifications concerning Summaryletouzey
2013-04-19interface.mli and serialize.ml reworked to avoid copy/paste of typesgareuselesinge
2013-04-18Only arguments declared as implicit can be renamedgareuselesinge
2013-04-17Matching patterns: fixed allow_partial_app which was not working onherbelin
2013-04-17Coqc: repair localisation of errors in filesletouzey
2013-04-17Improving error message in explain_cannot_find_well_typed_abstraction:herbelin
2013-04-15More functional implementation of locality_flag and program_modegareuselesinge
2013-04-11Backport r16394 from 8.4:msozeau
2013-04-03Fix for bug #3017: wrong handling of the unresolvability statusmsozeau
2013-04-02Revised infrastructure for lazy loading of opaque proofsletouzey
2013-04-02Exporting the SearchAbout filter.ppedrot
2013-03-26Moved the Loadpath part of Library to its own file, and documentedppedrot
2013-03-23Minor code cleaning in CArray / CList.ppedrot
2013-03-22Fix bug# 2994, 2971 about better error messages.msozeau
2013-03-21Robust display of NotConvertibleTypeField errors (fix #3008, #2995)letouzey
2013-03-21Typo dans message d'erreur (obligations).herbelin
2013-03-21Add type information in error message when a constructor is not fullyherbelin
2013-03-21Check unexpected "Local" keyword in cmd before opening a proof (fix #2975)letouzey
2013-03-19Removing the module Libtypes and unifying the Search[Pattern|Rewrite]?ppedrot
2013-03-18Making local variable warning verbose by default.ppedrot
2013-03-17Avoid a few overzealous "when Errors.noncritical"letouzey
2013-03-14Embedded exns in LtacLocated and EvaluatedError satisfy Errors.noncriticalletouzey
2013-03-14Cerrors: get rid of some FIXMEletouzey
2013-03-14Use Pp.msg instead of Pp.pp in -beautify (loss of text otherwise)letouzey
2013-03-13Modules and ppvernac, sequel of Enrico's commit 16261letouzey
2013-03-13Toplevel: improved commentsletouzey
2013-03-13Vernac+Toplevel: get rid of Error_in_fileletouzey
2013-03-13Vernac+Toplevel: get rid of DuringVernacInterpletouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 14)letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 13)letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 10)letouzey
2013-03-12invalid_arg instead of raise (Invalid_argement ...)letouzey
2013-03-12Allowing different types of, not to be mixed, generic Stores throughppedrot
2013-03-11Allowing (Co)Fixpoint to be defined local and Let-style.ppedrot
2013-03-11Obligations generated by Program are now local.ppedrot
2013-03-11Added a Local Definition vernacular command. This type of definitionppedrot
2013-03-08catch failures of pr_vernac to make -time failsafegareuselesinge
2013-03-05More monomorphization.ppedrot
2013-02-28Repairing r16205: errors raised by check_evar_instance were no longerherbelin
2013-02-28More informative error when a global reference is used in a context ofherbelin
2013-02-27Update debug code according to reorganization into modules.msozeau
2013-02-26kernel/declarations becomes a pure mliletouzey
2013-02-24Fixing bug #2466ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-11 07:12:44 +0000