aboutsummaryrefslogtreecommitdiff
path: root/printing
AgeCommit message (Expand)Author
2016-04-04Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Matthieu Sozeau
2016-04-04Merge branch 'linear-comparison' of https://github.com/aspiwack/coq into aspi...Matthieu Sozeau
2016-03-30Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-25Univs: fix get_current_context (bug #4603, part I)Matthieu Sozeau
2016-03-20Adding a new Ltac generic argument for forced tactics returing unit.Pierre-Marie Pédrot
2016-03-20Moving Refine to its proper module.Pierre-Marie Pédrot
2016-03-20Moving the Ltac definition command to an EXTEND based command.Pierre-Marie Pédrot
2016-03-20Moving Print Ltac to an EXTEND based command.Pierre-Marie Pédrot
2016-03-20Moving Tactic Notation to an EXTEND based command.Pierre-Marie Pédrot
2016-03-19Removing the untyped representation of genargs.Pierre-Marie Pédrot
2016-03-19Moving VernacSolve to an EXTEND-based definition.Pierre-Marie Pédrot
2016-03-18Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-13Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Hugo Herbelin
2016-03-10Primitive projections: protect kernel from erroneous definitions.Matthieu Sozeau
2016-03-06Moving Autorewrite to Hightatctic.Pierre-Marie Pédrot
2016-03-06Moving Tactic_debug to tactics/ folder.Pierre-Marie Pédrot
2016-03-04Removing the UConstr entry of the tactic_arg AST.Pierre-Marie Pédrot
2016-02-29Moving the "move" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "exists" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "symmetry" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "generalize dependent" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "clearbody" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "clear" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "cofix" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "fix" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-24Removing the MetaIdArg entry of tactic expressions.Pierre-Marie Pédrot
2016-02-22The tactic generic argument now returns a value rather than a glob_expr.Pierre-Marie Pédrot
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
2016-02-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-13Do not give a name to anonymous evars anymore. See bug #4547.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-29Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-23Implement support for universe binder lists in Instance and Program Fixpoint/...Matthieu Sozeau
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-21Stronger invariants on the use of the introduction pattern (pat1,...,patn).Hugo Herbelin
2016-01-20Update copyright headers.Maxime Dénès
2016-01-17Getting rid of the awkward unpack mechanism from Genarg.Pierre-Marie Pédrot
2016-01-17Temporary commit getting rid of Obj.magic unsafety for Genarg.Pierre-Marie Pédrot
2016-01-16Tactic notation printing accesses all the token data.Pierre-Marie Pédrot
2016-01-14Removing constr generic argument.Pierre-Marie Pédrot
2016-01-14Removing ident and var generic arguments.Pierre-Marie Pédrot
2016-01-11CLEANUP: removing unused fieldMatej Kosik
2016-01-11mergeMatej Kosik
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2016-01-02Use streams rather than strings to handle bullet suggestions.Guillaume Melquiond
2016-01-02Remove some unused functions.Guillaume Melquiond
2016-01-02Reduce dependencies of interface files.Guillaume Melquiond
2016-01-02Remove useless rec flags.Guillaume Melquiond
2016-01-02Simplification of grammar_prod_item type.Pierre-Marie Pédrot
2016-01-02Separation of concern in TacAlias API.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-27 13:52:16 +0000