aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2010-11-16Remove redundant clause (and fix compatibility issue)glondu
2010-11-15Minor fixes from Gregory Malecha. A typo fixed and a better (located) msozeau
2010-11-07Delayed the evar normalization in error messages to the last minuteherbelin
2010-11-07Add information of localisation when an error involving an "implicitherbelin
2010-11-07correcting a non catch error reported as an anomaly (Ploc.Exc)jforest
2010-11-03In Univ, unify order_request and constraint_typeglondu
2010-11-02Output universe graph in DOT language if output file ends in .dot or .gvglondu
2010-11-02More generic Univ.dump_universesglondu
2010-11-02Move stuff about positive into a distinct PArith subdirletouzey
2010-11-01Restored checking that _all_ arguments of the command line are meaningfulherbelin
2010-10-31Add tolerance for existential variables in Check.herbelin
2010-10-31Minor code improvements around libobjectherbelin
2010-10-31Minor factorization of the part of the code used for Unnamed_thm saving.herbelin
2010-10-26Compatibility camlp4/camlp5herbelin
2010-10-26Fail, when successful, prints something only in verbose modeglondu
2010-10-23Fixing bug #2412, continued (preprocessing of Ltac Debug errorsherbelin
2010-10-23Fixing bug #2412 (preprocessing of Ltac Debug errors forgotten in r13431).herbelin
2010-10-17About "unsupported" unicode characters in notations.herbelin
2010-10-11Backporting r13521 from branch 8.3 to trunk (fixing bug #2406, loopingherbelin
2010-10-07Fix bug# 2392msozeau
2010-10-06Remove Explain* vernacsglondu
2010-10-06Remove VernacGoglondu
2010-10-04Two [Evd.fold] turned into [Evd.fold_undefined].aspiwack
2010-10-03Avoid raising an anomaly when an error encapsulated with a dummyherbelin
2010-10-03Added multiple implicit arguments rules per name.herbelin
2010-10-03Making display of various informations about constants more modular:herbelin
2010-09-28Fix bug #2321, allowing "_" named projections in classes. Not realizingmsozeau
2010-09-28Remove some occurrences of "open Termops"glondu
2010-09-28Fix function applications without labels (OCaml warning 6)glondu
2010-09-24Fixed a bug in printing fix/cofix error messages when severalherbelin
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-09-18Fixing #2162 and #2367 (wrong order of Show Match) for branch 8.2 tooherbelin
2010-09-18Fixing bugs #2347 (part 2) and #2388: error message printing was doneherbelin
2010-09-14CoqIDE argv parsing delegated to coqtopvgross
2010-09-13Fix unescaped end-of-lines (OCaml warning 29)glondu
2010-09-02* removed declare_constant and declare_internal_constant vsiles
2010-09-02v13392 port from v8.3 to trunk : correct message when defining inductive schemesvsiles
2010-08-31* By default, load proof terms.regisgia
2010-08-27* scripts/Coqc toplevel/Usage:regisgia
2010-08-27* toplevel/Coqtop: Reactivate -dont-load-proofs option.regisgia
2010-08-27* lib/Flags: Replace dont_load_proofs by load_proofs since not loadingregisgia
2010-08-26Fix an error message ot having the ERror: prefix.courtieu
2010-07-29Rather quick hack to make basic unicode notations available byherbelin
2010-07-27Fix computation of fix annotation index: only consider assumptions andmsozeau
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-23Some fine-tuning after removal of automatic imports of coercions in r13310herbelin
2010-07-22Extension of the recursive notations mechanismherbelin
2010-07-22Simplified the way internalization_data (i.e. bindings of bound varsherbelin
2010-07-22Constrintern: unified push_name_env and push_loc_name_env; madeherbelin
2010-07-16Amelioration dans Functionjforest
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 21:04:55 +0000