aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
Commit message (Expand)AuthorAge
...
* | | Moving and enhancing the grammar_tactic_prod_item_expr type.Gravatar Pierre-Marie Pédrot2016-04-14
* | | Fixing printing of "destruct in" after ce71ac17268f.Gravatar Hugo Herbelin2016-04-12
* | | Removing the ad-hoc tactic_expr type.Gravatar Pierre-Marie Pédrot2016-04-11
* | | Extruding the print_atom primitive.Gravatar Pierre-Marie Pédrot2016-04-10
* | | Removing extra spaces in printing arguments of VERNAC EXTEND.Gravatar Hugo Herbelin2016-04-09
* | | Removing automatic printing of leading space in auto_using andGravatar Hugo Herbelin2016-04-09
* | | Simplifying code for printing VERNAC EXTEND.Gravatar Hugo Herbelin2016-04-09
* | | Fixing extra space in printing inductive types with no explicit type given.Gravatar Hugo Herbelin2016-04-09
* | | In pr_clauses, do not print a leading space by default so that it canGravatar Hugo Herbelin2016-04-09
* | | Fixing printing of toplevel values.Gravatar Pierre-Marie Pédrot2016-04-08
* | | Fixing printing of Tactic Notations with tactic arguments.Gravatar Pierre-Marie Pédrot2016-04-08
* | | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Gravatar Matthieu Sozeau2016-04-04
|\ \ \
* \ \ \ Merge branch 'linear-comparison' of https://github.com/aspiwack/coq into aspi...Gravatar Matthieu Sozeau2016-04-04
|\ \ \ \
* \ \ \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-30
|\ \ \ \ \ | | |_|/ / | |/| | |
| * | | | Univs: fix get_current_context (bug #4603, part I)Gravatar Matthieu Sozeau2016-03-25
* | | | | Adding a new Ltac generic argument for forced tactics returing unit.Gravatar Pierre-Marie Pédrot2016-03-20
* | | | | Moving Refine to its proper module.Gravatar Pierre-Marie Pédrot2016-03-20
* | | | | Moving the Ltac definition command to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* | | | | Moving Print Ltac to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* | | | | Moving Tactic Notation to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* | | | | Removing the untyped representation of genargs.Gravatar Pierre-Marie Pédrot2016-03-19
* | | | | Moving VernacSolve to an EXTEND-based definition.Gravatar Pierre-Marie Pédrot2016-03-19
* | | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-18
|\| | | |
* | | | | Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Gravatar Hugo Herbelin2016-03-13
| * | | | Primitive projections: protect kernel from erroneous definitions.Gravatar Matthieu Sozeau2016-03-10
* | | | | Moving Autorewrite to Hightatctic.Gravatar Pierre-Marie Pédrot2016-03-06
* | | | | Moving Tactic_debug to tactics/ folder.Gravatar Pierre-Marie Pédrot2016-03-06
* | | | | Removing the UConstr entry of the tactic_arg AST.Gravatar Pierre-Marie Pédrot2016-03-04
* | | | | Moving the "move" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* | | | | Moving the "exists" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* | | | | Moving the "symmetry" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* | | | | Moving the "generalize dependent" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* | | | | Moving the "clearbody" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* | | | | Moving the "clear" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* | | | | Moving the "cofix" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* | | | | Moving the "fix" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* | | | | Removing the MetaIdArg entry of tactic expressions.Gravatar Pierre-Marie Pédrot2016-02-24
* | | | | The tactic generic argument now returns a value rather than a glob_expr.Gravatar Pierre-Marie Pédrot2016-02-22
* | | | | merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\ \ \ \ \
* \ \ \ \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-13
|\ \ \ \ \ \ | | |/ / / / | |/| | | |
| * | | | | Do not give a name to anonymous evars anymore. See bug #4547.Gravatar Pierre-Marie Pédrot2016-02-13
| | * | | | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
| |/ / / / |/| | | |
* | | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\| | | |
| * | | | Implement support for universe binder lists in Instance and Program Fixpoint/...Gravatar Matthieu Sozeau2016-01-23
* | | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\| | | |
* | | | | Stronger invariants on the use of the introduction pattern (pat1,...,patn).Gravatar Hugo Herbelin2016-01-21
| * | | | Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | | | | Getting rid of the awkward unpack mechanism from Genarg.Gravatar Pierre-Marie Pédrot2016-01-17
* | | | | Temporary commit getting rid of Obj.magic unsafety for Genarg.Gravatar Pierre-Marie Pédrot2016-01-17
* | | | | Tactic notation printing accesses all the token data.Gravatar Pierre-Marie Pédrot2016-01-16