aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2013-05-09Updating some output tests in test-suite:herbelin
2013-05-09Use definition_entry to declare local definitionsgareuselesinge
2013-05-09Cosmetic changegareuselesinge
2013-05-09Getting rid of module Gmapl.ppedrot
2013-05-09A uniformization step around understand_* and interp_* functions.herbelin
2013-05-09A few comments in evarconv.mli.herbelin
2013-05-09Uniformization: isevars -> evdref/sigma/evdherbelin
2013-05-09Fixing r16487 on sharing evars between multiple parameters (missing List.rev).herbelin
2013-05-09Removing unused module Nbtermdn.ppedrot
2013-05-09Removing Gmap from Notations.ppedrot
2013-05-09Xml_datatype.mli ships the xml typegareuselesinge
2013-05-09add Loadpath to printers.mllibgareuselesinge
2013-05-08Uniformizing the [if_warn] flag used for warning printing and putppedrot
2013-05-08Protection against "Bad recursive type" in w_unify0 (bug #3036).herbelin
2013-05-08Alert when using ".." outside a Notation command.herbelin
2013-05-08Declaration of multiple hypotheses or parameters now share typingherbelin
2013-05-08Share more information between constructors and arity of an inductiveherbelin
2013-05-08Moved isolated test params_ind.v to Inductive.v.herbelin
2013-05-06Fixing ocamldoc compilation.ppedrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-26 22:43:51 +0000