aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
Commit message (Expand)AuthorAge
* Goal: remove most of the API (make [Goal.goal] concrete).Gravatar Arnaud Spiwack2014-10-16
* Emit a warning for void Arguments statement (Close 3713)Gravatar Enrico Tassi2014-10-13
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* 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
* Seeing IntroWildcard as an action intro pattern rather than as a naming patternGravatar Hugo Herbelin2014-09-30
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Notation: option to attach extra pretty printing rules to notationsGravatar Enrico Tassi2014-09-29
* Printing evar instance in a more intuitive order.Gravatar Hugo Herbelin2014-09-29
* Fix printing of primitive record info.Gravatar Matthieu Sozeau2014-09-29
* Print information about primitive records (Print and About).Gravatar Matthieu Sozeau2014-09-28
* Improve consistency of whitespace (beautifier).Gravatar Xavier Clerc2014-09-25
* Using an or_var rather than the hack with loc for coding a pure identGravatar Hugo Herbelin2014-09-24
* Fix a message.Gravatar Arnaud Spiwack2014-09-24
* coqtop -emacs: do not declare "still unfocused goals" as an "infomsg".Gravatar Arnaud Spiwack2014-09-24
* Fix debug printing with primitive projections.Gravatar Matthieu Sozeau2014-09-18
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
* Add a "Hint Mode ref (+ | -)*" hint for setting a global modeGravatar Matthieu Sozeau2014-09-15
* 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
* Add syntax [id]: to apply tactic to goal named id.Gravatar Hugo Herbelin2014-09-12
* Use evar name to print goal.Gravatar Hugo Herbelin2014-09-12
* Parsing evar instances.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Replace the list of argument in tacexpr with a single row argument.Gravatar Arnaud Spiwack2014-09-12
* VernacExtend does not dispatch on type anymore.Gravatar Pierre-Marie Pédrot2014-09-10
* Removing the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* Parsing of Type@{max(i,j)}.Gravatar Matthieu Sozeau2014-09-08
* 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
* Remove [Infer] option of records.Gravatar Arnaud Spiwack2014-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
* Add a [Variant] declaration which allows to write non-recursive variant types.Gravatar Arnaud Spiwack2014-09-04
* Fixing printing of unreachable local tactics.Gravatar Pierre-Marie Pédrot2014-09-03
* Cleaning code in Pptactic.Gravatar Pierre-Marie Pédrot2014-09-02
* Removing [revert] tactic from the AST.Gravatar Pierre-Marie Pédrot2014-09-02
* Moving the decompose tactic out of the AST.Gravatar Pierre-Marie Pédrot2014-09-01
* 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
* Type-safe version of genarg list / pair / opt functions.Gravatar Pierre-Marie Pédrot2014-08-29
* Simplification of Genarg unpackers.Gravatar Pierre-Marie Pédrot2014-08-29
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* Improve consistency of whitespace (beautifier).Gravatar Xavier Clerc2014-08-21
* Improve consistency of whitespace (beautifier).Gravatar Xavier Clerc2014-08-21
* Space after [identity] coercion keywords (beautifier).Gravatar Xavier Clerc2014-08-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 03:49:43 +0000