aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2016-02-15More conversion functions in the new tactic API.Pierre-Marie Pédrot
2016-02-15Moving conversion functions to the new tactic API.Pierre-Marie Pédrot
2016-02-15Renaming functions in Typing to stick to the standard e_* scheme.Pierre-Marie Pédrot
2016-02-15Monotonizing the Evarutil module.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-27Fix bug #4537: Coq 8.5 is slower in typeclass resolution.Pierre-Marie Pédrot
2016-01-24Fixing bug #4511: evar tactic can create non-typed evars.Pierre-Marie Pédrot
2016-01-23Implement support for universe binder lists in Instance and Program Fixpoint/...Matthieu Sozeau
2016-01-22Fixing a use of "clear" on an non-existing hypothesis in intro-patterns.Hugo Herbelin
2016-01-21New step on recent 9c2662eecc398f3 (strong invariants on tuple pattern).Hugo Herbelin
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-21Fixing some problems with double induction.Hugo Herbelin
2016-01-20Code simplification in elim.ml.Hugo Herbelin
2016-02-18Fixing a bug with introduction patterns over inductive types containing let-ins.Hugo Herbelin
2016-01-20Update copyright headers.Maxime Dénès
2016-01-19Fix bug #4420: check_types was losing universe constraints.Matthieu Sozeau
2016-01-17Moving val_cast to Tacinterp.Pierre-Marie Pédrot
2016-01-17Getting rid of the awkward unpack mechanism from Genarg.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-14Moving is_quantified_hypothesis to new proof engine.Hugo Herbelin
2016-01-14Update in the documentation of parts of the code of destruct/induction.Hugo Herbelin
2016-01-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-12Fix essential bug in new Keyed Unification mode reported by R. Krebbers.Matthieu Sozeau
2016-01-12Adding support for fresh for meta's and evar's.Pierre Courtieu
2016-01-11CLEANUP: removing unused fieldMatej Kosik
2016-01-11mergeMatej Kosik
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2016-01-11Fix bug #3338 again, no progress is necessary for the success of rewrite_strat.Matthieu Sozeau
2016-01-09Fix bug 4479: "Error: Rewriting base foo does not exist." should be catchable.Pierre-Marie Pédrot
2016-01-08Monotonizing Ftactic.Pierre-Marie Pédrot
2016-01-07Fix bug #4480: progress was not checked for setoid_rewrite.Matthieu Sozeau
2016-01-02Remove some unused functions.Guillaume Melquiond
2016-01-02Remove duplicate definition.Guillaume Melquiond
2016-01-02Remove duplicate declarations.Guillaume Melquiond
2016-01-02Reduce dependencies of interface files.Guillaume Melquiond
2016-01-02Remove useless rec flags.Guillaume Melquiond
2016-01-02Separation of concern in TacAlias API.Pierre-Marie Pédrot
2015-12-30Moving apply_type to new proof engine.Hugo Herbelin
2015-12-30Taking into account generated typing constraints in tactic "generalize".Hugo Herbelin
2015-12-30External tactics and notations now accept any tactic argument.Pierre-Marie Pédrot
2015-12-28Implementing non-focussed generic arguments.Pierre-Marie Pédrot
2015-12-28Removing the special status of open_constr generic argument.Pierre-Marie Pédrot
2015-12-28Eradicating uses of open_constr in TACTIC EXTEND in favour of uconstr.Pierre-Marie Pédrot
2015-12-27Factorizing code for untyped constr evaluation.Pierre-Marie Pédrot
2015-12-27Removing dead code.Pierre-Marie Pédrot
2015-12-27Tentative API fix for tactic arguments to be fed to tclWITHHOLES.Pierre-Marie Pédrot
2015-12-25Moving basic generalization tactics upwards for possible use in "intros".Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-12 13:13:13 +0000