aboutsummaryrefslogtreecommitdiff
path: root/printing
AgeCommit message (Expand)Author
2012-12-18Modulification of nameppedrot
2012-12-18Modulification of mod_bound_idppedrot
2012-12-18Modulification of Labelppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-12-14Moved Stringset and Stringmap to String namespace.ppedrot
2012-12-14Moved Intset and Intmap to Int namespace.ppedrot
2012-11-21Print univ constraints generated by a constant or inductive (when flag is set)barras
2012-11-20Cleaning and small optimization in CList.ppedrot
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-06remove useless hidden_flag in TacMutual(Co)Fixletouzey
2012-10-06Clean-up : removal of Proof_type.tactic_exprletouzey
2012-10-06Clean-up : no more Proof_type.proof_treeletouzey
2012-10-06Clean-up of proof_type.ml : no more Nested nor abstract_tactic_boxletouzey
2012-10-04Adding a nominal typing layer to Metasyntax in order to clarifyppedrot
2012-10-04Moved Compat to parsing. This permits to break the dependency of theppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-10-01Added a new tactical infoH tac, that displays the names of hypothesis created...courtieu
2012-09-20Fixing Show Script issues.ppedrot
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-09-14Partial revert of Yann commit in order to use CLib.List when openingppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-08-24correct some ends of .mllib files (avoid a broken tolink.ml)letouzey
2012-08-11Added support for option Local (at module level) in Tactic Notation.herbelin
2012-08-08Updating headers.herbelin
2012-08-07Avoid Pp.std_ppcmds in Misctypes.sort_infoletouzey
2012-07-30Bigint: avoid dependency over Ppletouzey
2012-07-21Slight modification to the printing of goals when in emacs mode.courtieu
2012-07-20Fixing test-suitepboutill
2012-07-19Getting rid of the undocumented [complete] tactic, which wasppedrot
2012-07-11A friendlier printing of remaining goals when no goal is focused.aspiwack
2012-07-10Fixing Print Assumption displayppedrot
2012-07-10Small change in the printing of proofs for use by coqide.aspiwack
2012-07-10Another correction to the dependent existential variable printingaspiwack
2012-07-09The tactic remember now accepts a final eqn:H option (grant wish #2489)letouzey
2012-07-09induction/destruct : nicer syntax for generating equations (solves #2741)letouzey
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-07-04Change how the number of open goals is printed.aspiwack
2012-07-04When focused on an empty list of goal (after finishing a subproof introducedaspiwack
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 01:43:51 +0000