aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2011-10-05Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).herbelin
2011-10-01Fixing critical part of bug #2504. Not all inductive types in Type areherbelin
2011-09-27In Coq_config: get rid of coqsrc and make coqlib optionalglondu
2011-09-26Added support for referring to subterms of the goal by pattern.herbelin
2011-09-26Moving implicit tactic support from Tacinterp to Pfedit and final evarherbelin
2011-09-15Re-allowing assumptions during proofs seems safe now (fix #2411)letouzey
2011-09-12Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...aspiwack
2011-09-05Coqide: new backtracking code, based on the Backtrack commandletouzey
2011-09-05Ide_intf: slight reorganisation of the IDE apiletouzey
2011-09-05Lib.node: merge OpenedModtype and OpenedModule, same for Closed...letouzey
2011-09-05Remove code concerning the obsolete Set/Unset Undoletouzey
2011-08-30Quick improvement of some error messages related to module applicationherbelin
2011-08-23Clarifying that only identifiers are advertised to be turned into keywordsherbelin
2011-08-18Misc improvements concerning "Show Match" and its coqide equivalentletouzey
2011-08-11SearchAbout and similar: add a customizable blacklistletouzey
2011-08-10Improving error message about coinductive guard (old "cases" is now "match")herbelin
2011-08-10Partly revert commit r14389 about relaxing the condition for being a keywordherbelin
2011-08-09Moved the declaration of "Classic" being the default proof mode to coqtop.ml ...aspiwack
2011-08-08Be a bit less aggressive in declaring idents as keywords in notationsherbelin
2011-08-03Fix nf_evars_undefined use in pr_constraintsmsozeau
2011-07-29Class: generic equality on constr replaced by destructorspuech
2011-07-28Ide_slave: same attributes for { } and Focus/Unfocus (fix coqide display)letouzey
2011-07-16This option disables the use of the '{| field := ... |}' notationherbelin
2011-06-30Keep obligation source information in Programmsozeau
2011-06-21Cleaning debugging printer relative to new proof engine. Inherbelin
2011-06-20Add compatibility option "-compat 8.3".herbelin
2011-06-18Relaxed the constraint introduced in r14190 that froze the existingherbelin
2011-06-14Fixing bug #2181 (Class mechanism can create dependencies over unnamedherbelin
2011-06-13Another bug of Scheme Induction (generated names dep/nodep were swapped).herbelin
2011-06-13Fixing an anomaly in Scheme Induction.herbelin
2011-05-24Made the emacs-U option deprecated. Also removed the old codecourtieu
2011-05-18Coqide: allow the use of Abort (grant wish #2357)letouzey
2011-05-17More work on error handlingletouzey
2011-05-17Break circular dependency Proof_global -> Vernacexpr -> Proof_global.aspiwack
2011-05-16Repair the "Fail" command after recent changes in exception handlingletouzey
2011-05-16turn the automatic generation of boolean equalityvsiles
2011-05-15Turning Sys_error into error by default instead of anomaly. After all,herbelin
2011-05-13A new mechanism to handle errors.aspiwack
2011-05-13New option [Set Bullet Behavior] allows to select the behaviour of bullets.aspiwack
2011-05-11Print Module (Type) M now tries to print more detailsletouzey
2011-05-05Merge branch 'subclasses' into coq-trunkmsozeau
2011-04-29Fixed a bug causing inconsistent states during proof editting.aspiwack
2011-04-28coqtop -config returns coq returns coq environments at exection timepboutill
2011-04-28Fixed notation printing bug when curly brackets are involved (requestsherbelin
2011-04-21Coqide: better handling of stdout/stderr in win32letouzey
2011-04-18Add a flag to control betaiota reduction during unification to maintain backw...msozeau
2011-04-14Add directories in COQPATH to search path.herbelin
2011-04-14Reorder search path order, so the standard library is search last.herbelin
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
2011-04-13- Make typeclass transparency information directly availablemsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 08:38:09 +0000