aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
2011-11-18Adding the type infrastructure to handle properly API management of optionsppedrot
2011-11-18Fix parsing of :>> and backtrack correctly on the cache of hints for local co...msozeau
2011-11-18Added a printing function to handle single evarsppedrot
2011-11-18Restore backward compatibility. ":>" declares subinstances in Class declarati...msozeau
2011-11-17Fixing bug #2640 and variants of it (inconsistency between when andherbelin
2011-11-17Merge subinstances branch by me and Tom Prince.msozeau
2011-11-16Fixing beautification of "thm_token" (missing space) + improvements.herbelin
2011-11-07Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructorsletouzey
2011-10-28Remove dynamic stuff from constr_expr and glob_constrglondu
2011-10-25Applying Tom Prince's patch to support parametric "constructor n" inherbelin
2011-10-25First attempt at making Print Assumption compatible with opaque modules (fix ...letouzey
2011-10-11Various simplifications about constant_of_delta and mind_of_deltaletouzey
2011-09-15Names.make_mbid and co : convert from/to identifier (avoid some String.copy)letouzey
2011-09-12Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...aspiwack
2011-09-05Lib.node: merge OpenedModtype and OpenedModule, same for Closed...letouzey
2011-08-30Porting Hendrik's 8.3 patch for proof tree visualization under proofherbelin
2011-08-30Quick improvement of some error messages related to module applicationherbelin
2011-08-13New fix for is_ident_not_keyword.herbelin
2011-08-10Propagated information from the reduction tactics to the kernel soherbelin
2011-08-09In coqtop, a terminating "." must now be followed by a blank or eof.letouzey
2011-08-08Be a bit less aggressive in declaring idents as keywords in notationsherbelin
2011-07-29Term: Refactoring of hashconsingpuech
2011-07-27Oversight in revision 14292.pboutill
2011-07-26Partial revert of r14292pboutill
2011-07-22Add a syntax entry for fully applied constructor patternpboutill
2011-07-05Adding a new syntax for BeginSubproof and EndSubproof, namely { and }.courtieu
2011-06-10Revert "Check if recursive calls are guarded before printing "Proof completed"."pboutill
2011-05-26Check if recursive calls are guarded before printing "Proof completed".herbelin
2011-05-24Made the emacs-U option deprecated. Also removed the old codecourtieu
2011-05-21Restore display of notation when printing an inductive such as sigletouzey
2011-05-17Break circular dependency Proof_global -> Vernacexpr -> Proof_global.aspiwack
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-04-26Pcoq.ml4: fix a typo in a comment to please ocamldocletouzey
2011-04-26G_vernac can be parsed without grammar.cmaletouzey
2011-04-24Fixing bug in printing let-in binders in fix/cofixherbelin
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
2011-04-13Add [Polymorphic] flag for defsmsozeau
2011-04-08Made warning about ending comments in string less intrusive so as to supportherbelin
2011-04-08Fixing multiple printing bugs with "Notation f x := ..."herbelin
2011-04-06Add 'Existing Instances' declaration to declare multiple instances at once.letouzey
2011-04-03Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksletouzey
2011-03-23- Remove useless grammar rulemsozeau
2011-03-18A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> secondsletouzey
2011-03-13- Add modulo_delta_types flag for unification to allow fullmsozeau
2011-03-07Reverted commit r13893 about propagation of more informativeherbelin
2011-03-07Added propagation of evars unification failure reasons for betterherbelin
2011-03-05Forgotten removal of ',' in 'fun' rule: it has to come with the lambda notationherbelin
2011-02-14- Fix treatment of globality flag for typeclass instance hints (theymsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 10:21:08 +0000