aboutsummaryrefslogtreecommitdiff
path: root/printing/printer.ml
AgeCommit message (Expand)Author
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
2014-03-31Removing the Change_evar refiner rule.Pierre-Marie Pédrot
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-03-02Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codePierre Letouzey
2014-01-17Follow-up of bugfix for #3204: local definitions were not handled properly.Pierre-Marie Pédrot
2014-01-16Fixing bugs #1039: Hypotheses don't respect Barendregt conventionPierre-Marie Pédrot
2013-11-02Adds a tactic give_up.aspiwack
2013-11-02Adds a shelve tactic.aspiwack
2013-10-27Abstracting evar filter away. The API is not perfect, but better than nothing.ppedrot
2013-10-05Moving side effects into evar_map. There was no reason to keep anotherppedrot
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-09-03Partly replacing list-based access functions in Evd. This is stillppedrot
2013-09-03Some cleanup in Autoppedrot
2013-08-22Nicer code concerning dirpaths and modpath around Libletouzey
2013-08-08State Transaction Machinegareuselesinge
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 07:27:51 +0000