aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
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
2010-07-05Fix goal display when backtrackingvgross
2010-07-05Stronger checks on coqtop termination, warning when zombies.vgross
2010-06-29Correct wrong handling of evars in instance definitions that preventedmsozeau
2010-06-29change the flag "internal" in declare/ind_tables from bool tovsiles
2010-06-29Made tclABSTRACT normalize evars before saying it does not supportherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-06-12Fixed bug #2135 (second-order unification was raising cryptic message)herbelin
2010-06-12Added regression tests for bugs + miscellaneous improvementsherbelin
2010-06-12Applying François' patch fixing grammar of uniform inheritance condition mes...herbelin
2010-06-12Fixing spelling: pr_coma -> pr_commaherbelin
2010-06-09Automatic introduction of names given before ":" in Lemma's andherbelin
2010-06-08Fix treatment of {struct x} annotations in presence of generalizedmsozeau
2010-06-07fixing error message display.vgross
2010-06-06Added support for Ltac-matching terms with variables bound in the patternherbelin
2010-06-03Added command "Locate Ltac qid".herbelin
2010-06-03Ide_blob: avoid direct use of Stdpp for compatibility with new camlp4letouzey
2010-06-01Cleanup: remove code specific for ocaml 3.06letouzey
2010-06-01restore handling of lexer errorsletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 23:15:31 +0000