aboutsummaryrefslogtreecommitdiff
path: root/printing/printer.ml
AgeCommit message (Expand)Author
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-03-31Declarative mode: plug the specialised printers back.Arnaud Spiwack
2015-03-31Better formatting of messages in proofs.Arnaud Spiwack
2015-03-31Generalisation of the "end command" argument of the goal printer.Arnaud Spiwack
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-24Isolate a function for printing evar sets.Hugo Herbelin
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2015-01-08Continuing 785f82ee1 on reverting not only f5d7b2b1e but alsoHugo Herbelin
2015-01-08Fixed and extend bullet related info/error messages. + doc.Pierre Courtieu
2014-12-27Revert "Term: include a function to print terms"Enrico Tassi
2014-12-26Term: include a function to print termsEnrico Tassi
2014-12-18Fixed bad newlines in output for std output and emacs.Pierre Courtieu
2014-12-16msg_info now puts infomsg tag in emacs mode.Pierre Courtieu
2014-12-15Changed bullet informations to warning for better display in PG.Pierre Courtieu
2014-11-22Removing useless flag of the historical move tactic.Pierre-Marie Pédrot
2014-11-20Moving mutual inductive printing from Printer to Printmod.Pierre-Marie Pédrot
2014-11-19Print [uconstr] in genargs.Arnaud Spiwack
2014-11-19Printing function for [uconstr].Arnaud Spiwack
2014-11-07Removing the legacy intro tactic code.Pierre-Marie Pédrot
2014-11-04Removing the old rename tactic.Pierre-Marie Pédrot
2014-11-01Info: print a name for the primitive tactics in [Proofview].Arnaud Spiwack
2014-10-22Pushing Pierre's factorization of names in goal context printing fromHugo Herbelin
2014-10-17Experimental printing of the signature of open evars in Check.Hugo Herbelin
2014-10-16Goal: remove most of the API (make [Goal.goal] concrete).Arnaud Spiwack
2014-10-09Removing Convert_concl and Convert_hyp from Logic.Hugo Herbelin
2014-10-01Going back on granting wish #1039 in f5d7b2b1e so that apply withHugo Herbelin
2014-09-24Fix a message.Arnaud Spiwack
2014-09-24coqtop -emacs: do not declare "still unfocused goals" as an "infomsg".Arnaud Spiwack
2014-09-17Revert specific syntax for primitive projections, avoiding uglyMatthieu Sozeau
2014-09-15Not printing goal name (reinstalled by mistake in a previous commit).Hugo Herbelin
2014-09-15Fixing bug #3619 in emacs mode.Hugo Herbelin
2014-09-13Prepare goal name printing but no not print them at the current time.Hugo Herbelin
2014-09-13Checking typability of evar instances. Using ";" to separate bindingsHugo Herbelin
2014-09-12Use evar name to print goal.Hugo Herbelin
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-09-05Removing the old implementation of clear_body.Pierre-Marie Pédrot
2014-09-04Revert the two previous commits. I was testing in the wrong branch.Pierre-Marie Pédrot
2014-09-04Removing the old implementation of clear_body.Pierre-Marie Pédrot
2014-09-04Inductive and CoInductive records are printed correctly.Arnaud Spiwack
2014-09-04Print [Variant] types with the keyword [Variant].Arnaud Spiwack
2014-09-01Coqide prints succesive hyps of the same type on 1 linePierre Boutillier
2014-08-30Simplify even further the declaration of primitive projections,Matthieu Sozeau
2014-08-03Move to a representation of universe polymorphic constants using indices for ...Matthieu Sozeau
2014-07-11Feedback: LoadedFile + GoalsEnrico Tassi
2014-06-17Removing dead code.Pierre-Marie Pédrot
2014-05-06Initial work on reintroducing old-style polymorphism for compatibility (the s...Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-23Better representation of evar filters: we represent the vacuous filters ofPierre-Marie Pédrot
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 06:05:37 +0000