aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/printer.ml
Commit message (Expand)AuthorAge
...
* Term: include a function to print termsGravatar Enrico Tassi2014-12-26
* Fixed bad newlines in output for std output and emacs.Gravatar Pierre Courtieu2014-12-18
* msg_info now puts infomsg tag in emacs mode.Gravatar Pierre Courtieu2014-12-16
* Changed bullet informations to warning for better display in PG.Gravatar Pierre Courtieu2014-12-15
* Removing useless flag of the historical move tactic.Gravatar Pierre-Marie Pédrot2014-11-22
* Moving mutual inductive printing from Printer to Printmod.Gravatar Pierre-Marie Pédrot2014-11-20
* Print [uconstr] in genargs.Gravatar Arnaud Spiwack2014-11-19
* Printing function for [uconstr].Gravatar Arnaud Spiwack2014-11-19
* Removing the legacy intro tactic code.Gravatar Pierre-Marie Pédrot2014-11-07
* Removing the old rename tactic.Gravatar Pierre-Marie Pédrot2014-11-04
* Info: print a name for the primitive tactics in [Proofview].Gravatar Arnaud Spiwack2014-11-01
* Pushing Pierre's factorization of names in goal context printing fromGravatar Hugo Herbelin2014-10-22
* Experimental printing of the signature of open evars in Check.Gravatar Hugo Herbelin2014-10-17
* Goal: remove most of the API (make [Goal.goal] concrete).Gravatar Arnaud Spiwack2014-10-16
* Removing Convert_concl and Convert_hyp from Logic.Gravatar Hugo Herbelin2014-10-09
* Going back on granting wish #1039 in f5d7b2b1e so that apply withGravatar Hugo Herbelin2014-10-01
* Fix a message.Gravatar Arnaud Spiwack2014-09-24
* coqtop -emacs: do not declare "still unfocused goals" as an "infomsg".Gravatar Arnaud Spiwack2014-09-24
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
* Not printing goal name (reinstalled by mistake in a previous commit).Gravatar Hugo Herbelin2014-09-15
* Fixing bug #3619 in emacs mode.Gravatar Hugo Herbelin2014-09-15
* Prepare goal name printing but no not print them at the current time.Gravatar Hugo Herbelin2014-09-13
* Checking typability of evar instances. Using ";" to separate bindingsGravatar Hugo Herbelin2014-09-13
* Use evar name to print goal.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Removing the old implementation of clear_body.Gravatar Pierre-Marie Pédrot2014-09-05
* Revert the two previous commits. I was testing in the wrong branch.Gravatar Pierre-Marie Pédrot2014-09-04
* Removing the old implementation of clear_body.Gravatar Pierre-Marie Pédrot2014-09-04
* Inductive and CoInductive records are printed correctly.Gravatar Arnaud Spiwack2014-09-04
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
* Coqide prints succesive hyps of the same type on 1 lineGravatar Pierre Boutillier2014-09-01
* Simplify even further the declaration of primitive projections,Gravatar Matthieu Sozeau2014-08-30
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* Feedback: LoadedFile + GoalsGravatar Enrico Tassi2014-07-11
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Better representation of evar filters: we represent the vacuous filters ofGravatar Pierre-Marie Pédrot2014-04-23
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Removing the Change_evar refiner rule.Gravatar Pierre-Marie Pédrot2014-03-31
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codeGravatar Pierre Letouzey2014-03-02
* Follow-up of bugfix for #3204: local definitions were not handled properly.Gravatar Pierre-Marie Pédrot2014-01-17
* Fixing bugs #1039: Hypotheses don't respect Barendregt conventionGravatar Pierre-Marie Pédrot2014-01-16
* Adds a tactic give_up.Gravatar aspiwack2013-11-02
* Adds a shelve tactic.Gravatar aspiwack2013-11-02
* Abstracting evar filter away. The API is not perfect, but better than nothing.Gravatar ppedrot2013-10-27
* Moving side effects into evar_map. There was no reason to keep anotherGravatar ppedrot2013-10-05
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 05:59:05 +0000