aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.ml
Commit message (Expand)AuthorAge
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\
| * Fix bug #4707: clearbody much slower in 8.5pl1.Gravatar Pierre-Marie Pédrot2016-05-03
* | Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Gravatar Hugo Herbelin2016-04-27
* | In the short term, stronger invariant on the syntax of TacAssert, whatGravatar Hugo Herbelin2016-04-27
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-09
|\|
| * Fixing the "No applicable tactic" non informative error messageGravatar Hugo Herbelin2016-04-03
* | Moving Refine to its proper module.Gravatar Pierre-Marie Pédrot2016-03-20
* | Making Proofview independent of Logic.Gravatar Pierre-Marie Pédrot2016-03-20
* | merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\ \
* | | Using monotonic types for conversion functions.Gravatar Pierre-Marie Pédrot2016-02-15
* | | Code factorization of tactic "unfold_body".Gravatar Pierre-Marie Pédrot2016-02-15
* | | More conversion functions in the new tactic API.Gravatar Pierre-Marie Pédrot2016-02-15
* | | Moving conversion functions to the new tactic API.Gravatar Pierre-Marie Pédrot2016-02-15
* | | Renaming functions in Typing to stick to the standard e_* scheme.Gravatar Pierre-Marie Pédrot2016-02-15
* | | Monotonizing the Evarutil module.Gravatar Pierre-Marie Pédrot2016-02-15
| * | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
|/ /
* | Fixing a use of "clear" on an non-existing hypothesis in intro-patterns.Gravatar Hugo Herbelin2016-01-22
* | 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
* | Fixing a bug with introduction patterns over inductive types containing let-ins.Gravatar Hugo Herbelin2016-02-18
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| * Fix bug #4420: check_types was losing universe constraints.Gravatar Matthieu Sozeau2016-01-19
* | Moving is_quantified_hypothesis to new proof engine.Gravatar Hugo Herbelin2016-01-14
* | Update in the documentation of parts of the code of destruct/induction.Gravatar Hugo Herbelin2016-01-14
* | mergeGravatar Matej Kosik2016-01-11
|\ \
| * | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | | Remove useless rec flags.Gravatar Guillaume Melquiond2016-01-02
* | | Moving apply_type to new proof engine.Gravatar Hugo Herbelin2015-12-30
* | | Taking into account generated typing constraints in tactic "generalize".Gravatar Hugo Herbelin2015-12-30
* | | Moving basic generalization tactics upwards for possible use in "intros".Gravatar Hugo Herbelin2015-12-25
* | | Moving code of specialize so that it can accept "as" (no semantic change).Gravatar Hugo Herbelin2015-12-25
* | | Moving specialize to Proofview.tactic.Gravatar Hugo Herbelin2015-12-25
* | | Fixing a bug in the order of side conditions for introduction pattern -> and <-.Gravatar Hugo Herbelin2015-12-25
|/ /
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-11
|\|
| * Add tactic native_cast_no_check, analog to vm_cast_no_check.Gravatar Maxime Dénès2015-12-11
| * Silently ignore requests to _not_ clear something when that something cannot ...Gravatar Guillaume Melquiond2015-12-10
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-08
|\|
| * Fix some typos.Gravatar Guillaume Melquiond2015-12-07
* | Removing redundant versions of generalize.Gravatar Hugo Herbelin2015-12-05
* | Experimenting removing strong normalization of the mid-statement in tactic cut.Gravatar Hugo Herbelin2015-12-05
* | Moving three related small half-general half-ad-hoc utility functionsGravatar Hugo Herbelin2015-12-05
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-03
|\|
| * Slight simplification of code for pat/constr.Gravatar Hugo Herbelin2015-12-02
| * Dead code from August 2014 in apply in.Gravatar Hugo Herbelin2015-12-02
* | Removing a use of old refine in Tactics.Gravatar Pierre-Marie Pédrot2015-11-23
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-20
|\|
| * More optimizations of [Clenv.clenv_fchain].Gravatar Pierre-Marie Pédrot2015-11-17
| * Performance fix for destruct.Gravatar Pierre-Marie Pédrot2015-11-17
* | Activating bracketing of last or-and introduction pattern by defaultGravatar Hugo Herbelin2015-11-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 05:14:43 +0000