aboutsummaryrefslogtreecommitdiff
path: root/printing/ppvernac.ml
AgeCommit message (Expand)Author
2013-11-02Fixes parsing of all: followed by a typechecking/evaluation command.aspiwack
2013-11-02New option Default Goal Selector.aspiwack
2013-11-02Adds a new goal selector "all:".aspiwack
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-10-24Turn many List.assoc into List.assoc_fletouzey
2013-10-10STM: add "Stm Wait" to wait for the slaves to complete their jobsgareuselesinge
2013-10-07STM: new command "Stm PrintDag" to force printing the dag to /tmpgareuselesinge
2013-08-19Modulification and removing of structural equality in Stateid.ppedrot
2013-08-08Support Proof Generalgareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-08-01Added a Print Debug GC command that displays the current state ofppedrot
2013-08-01Granting bug #3098: adding priority to Existing Instances.ppedrot
2013-07-17More dynamic argument scopesletouzey
2013-07-10Added a Register Inline command for the native compiler. Will be ported to th...mdenes
2013-04-17Renaming SearchAbout into Search and Search into SearchHead.herbelin
2013-04-15More functional implementation of locality_flag and program_modegareuselesinge
2013-03-17Ppvernac: no globalization for printing ltac definitionsletouzey
2013-03-14Pptactic.pr_raw_tactic is now without env argumentletouzey
2013-03-13Modules and ppvernac, sequel of Enrico's commit 16261letouzey
2013-03-11Allowing (Co)Fixpoint to be defined local and Let-style.ppedrot
2013-03-11Added a Local Definition vernacular command. This type of definitionppedrot
2013-03-08Use with_state_protection in pr_module_vardeclsgareuselesinge
2013-03-05More monomorphization.ppedrot
2013-02-18Removing Exc_located and using the new exception enrichementppedrot
2013-02-10Useless use of hooks in VernacDefinition. In addition, this wasppedrot
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-18Modulification of mod_bound_idppedrot
2012-12-14Modulification of identifierppedrot
2012-11-13Added a CString module.ppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-10-31Change [Hints Resolve] to still accept constrs as argumentsmsozeau
2012-10-29Fixed #2926:ppedrot
2012-10-26Change Hint Resolve, Immediate to take a global reference as argumentmsozeau
2012-10-16Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterpletouzey
2012-10-06still some more dead code removalletouzey
2012-10-04Moved Compat to parsing. This permits to break the dependency of theppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-11Added support for option Local (at module level) in Tactic Notation.herbelin
2012-08-08Updating headers.herbelin
2012-07-09Avoid a warning about unprintable new command Print Namespaceletouzey
2012-07-05Notation: a new annotation "compat 8.x" extending "only parsing"letouzey
2012-07-04Fixes a bug in Ppvernac which had braces and bullets printed with an endingaspiwack
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-19Fixing some inconsistencies of constr printer wrt constr parserherbelin
2012-05-29place all pretty-printing files in new dir printing/letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 08:16:50 +0000