aboutsummaryrefslogtreecommitdiff
path: root/printing/prettyp.mli
AgeCommit message (Collapse)Author
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
instances still to do). Using heuristics to name after the quantifier name it comes. Also added a "sigma" to almost all printing functions.
2014-07-21Unifying locate code, also making it more powerful: it is now able to findPierre-Marie Pédrot
any prefix of the given qualid.
2014-07-21Adding a new "Locate Term" command, distinct from the raw "Locate" command.Pierre-Marie Pédrot
The new Term version has essentially the same behaviour as the old "Locate", while the new raw searches for all types of objects. Also code merging with the "Locate Ltac". Fixes bug #3380.
2014-07-21More complete printing of Ltac location, akin to the term-dedicated Locate ↵Pierre-Marie Pédrot
command.
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
2013-04-29Merging Context and Sign.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16463 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-18Modulification of nameppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16099 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14Modulification of identifierppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29place all pretty-printing files in new dir printing/letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15391 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 20:37:25 +0000