aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
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
2010-05-31CoqIDE goes multiprocessvgross
2010-05-31More indirection.vgross
2010-05-31Introducing strong typing for IDE - toplevel IPCvgross
2010-05-31deporting Coq specific code from ide to toplevel.vgross
2010-05-31Modifying startup sequencevgross
2010-05-29New pass on inductive schemesherbelin
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
2010-05-19Nicer representation of tokens, more independant of camlp*letouzey
2010-05-19static (and shared) camlp4use instead of per-file declarationletouzey
2010-05-19Remove compile-command pragmas for emacsletouzey
2010-05-18Applicative commutative cuts in Fixpoint guard conditionpboutill
2010-05-04 - Fixing bug #2308 about Lemma ... withvsiles
2010-04-30Fail: a way to check that a command is refused without blocking a scriptletouzey
2010-04-29Various minor improvements of comments in mli for ocamldocletouzey
2010-04-29Two forgotten $Id$ in last commitletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2010-04-27Fix bug #2245, incorrect handling of Context in sections inside modulemsozeau
2010-04-27Added a new exception for already declared Schemes, vsiles
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 00:29:19 +0000