aboutsummaryrefslogtreecommitdiff
path: root/tactics/tactics.ml
AgeCommit message (Expand)Author
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-05-04Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-03Fix bug #4707: clearbody much slower in 8.5pl1.Pierre-Marie Pédrot
2016-04-27Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Hugo Herbelin
2016-04-27In the short term, stronger invariant on the syntax of TacAssert, whatHugo Herbelin
2016-04-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-03Fixing the "No applicable tactic" non informative error messageHugo Herbelin
2016-03-20Moving Refine to its proper module.Pierre-Marie Pédrot
2016-03-20Making Proofview independent of Logic.Pierre-Marie Pédrot
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
2016-02-15Using monotonic types for conversion functions.Pierre-Marie Pédrot
2016-02-15Code factorization of tactic "unfold_body".Pierre-Marie Pédrot
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-22Fixing a use of "clear" on an non-existing hypothesis in intro-patterns.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-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-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-11mergeMatej Kosik
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2016-01-02Remove useless rec flags.Guillaume Melquiond
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-25Moving basic generalization tactics upwards for possible use in "intros".Hugo Herbelin
2015-12-25Moving code of specialize so that it can accept "as" (no semantic change).Hugo Herbelin
2015-12-25Moving specialize to Proofview.tactic.Hugo Herbelin
2015-12-25Fixing a bug in the order of side conditions for introduction pattern -> and <-.Hugo Herbelin
2015-12-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-11Add tactic native_cast_no_check, analog to vm_cast_no_check.Maxime Dénès
2015-12-10Silently ignore requests to _not_ clear something when that something cannot ...Guillaume Melquiond
2015-12-08Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-07Fix some typos.Guillaume Melquiond
2015-12-05Removing redundant versions of generalize.Hugo Herbelin
2015-12-05Experimenting removing strong normalization of the mid-statement in tactic cut.Hugo Herbelin
2015-12-05Moving three related small half-general half-ad-hoc utility functionsHugo Herbelin
2015-12-03Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-02Slight simplification of code for pat/constr.Hugo Herbelin
2015-12-02Dead code from August 2014 in apply in.Hugo Herbelin
2015-11-23Removing a use of old refine in Tactics.Pierre-Marie Pédrot
2015-11-20Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-17More optimizations of [Clenv.clenv_fchain].Pierre-Marie Pédrot
2015-11-17Performance fix for destruct.Pierre-Marie Pédrot
2015-11-10Activating bracketing of last or-and introduction pattern by defaultHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 15:39:51 +0000