aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2013-05-06Small cleaning of Evd interface.ppedrot
2013-05-06fake_ide: xml parser does not check for EOFgareuselesinge
2013-05-06New module Xml_printer (dual to Xml_parser)gareuselesinge
2013-05-06Coqide: view -> zoom in / out / fitgareuselesinge
2013-05-06States: frozen states can hold closuresgareuselesinge
2013-05-06Summary: support selective freezegareuselesinge
2013-05-06Ideutils: comment on missing Glib utf8 handling functiongareuselesinge
2013-05-06Close the .glob file after having saved .vogareuselesinge
2013-05-06Fix typo in manualgareuselesinge
2013-05-05Improving printing of 'rew' notationherbelin
2013-05-05Hack to solve a "Bad recursive type" anomaly.herbelin
2013-05-05Now printing body of abbreviations (i.e. notation with a name) withherbelin
2013-05-05Little fix for Nsatz: hypotheses not directly relevant to the nsatzherbelin
2013-05-05Improvement of r16204 on reporting tactic error locations: if the mainherbelin
2013-05-05Relaxing the constraint on eta-expanding on the fly while looking forherbelin
2013-05-05Reporting the change on matching partial applications in patterns ofherbelin
2013-05-03Removing a redundant function from Evd.ppedrot
2013-04-30Fix wrong computation of dependency signature in cases raising an uncaught ex...msozeau
2013-04-29Merging Context and Sign.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-04-27Added a unit test for bug #2230.ppedrot
2013-04-25Fix compilation (vernac.ml, missing ;)gareuselesinge
2013-04-25Fix: tooltip correctly handles the absence of info (empty string)gareuselesinge
2013-04-25Coqide: Globalization feedback (proof of concept)gareuselesinge
2013-04-25lablgtk2 misses Glib.Utf8.pos_to_offset, workaround in ideutilsgareuselesinge
2013-04-25Flag ide_slave moved into Flags modulegareuselesinge
2013-04-25Coqide: new tag "tooltip" for the Script windowgareuselesinge
2013-04-25raise UnsafeSuccess -> feedback AddedAxiomgareuselesinge
2013-04-25Coqide: new feedback mechanism for structured contentgareuselesinge
2013-04-25Fix indentationgareuselesinge
2013-04-23Fix issues with "Reset Initial" in scripts given to coqtop -lletouzey
2013-04-23Egramcoq+Lexer : no need for an init_functionletouzey
2013-04-23Indfun : use States.with_state_protection instead of freeze/unfreezeletouzey
2013-04-23Egramcoq: clean an ugly code snippetletouzey
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-22Declaremods: some more minor cleanupletouzey
2013-04-19Fix compilation of fake_idegareuselesinge
2013-04-19interface.mli and serialize.ml reworked to avoid copy/paste of typesgareuselesinge
2013-04-18coqc and coqmktop migrated in tools/, get rid of scripts/ subdirletouzey
2013-04-18Coqdep: add an -exclude-dir option (wish mentionned in #3025)letouzey
2013-04-18Coqc: accept -exclude-dir + some others + cleanup (fix #3025)letouzey
2013-04-18Finer fix for bug 3017, mark unresolvability only of goals that aremsozeau
2013-04-18Only arguments declared as implicit can be renamedgareuselesinge
2013-04-18Fix #3001 (rename arg of global cst inside section)gareuselesinge
2013-04-17Renaming SearchAbout into Search and Search into SearchHead.herbelin
2013-04-17Matching patterns: fixed allow_partial_app which was not working onherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-31 08:59:22 +0000