aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Removing tclEVARS in various places.Gravatar Pierre-Marie Pédrot2015-10-19
* Reducing the uses of tclEVARS in Tactics by using monotonous functions.Gravatar Pierre-Marie Pédrot2015-10-19
* Making Evarutil.new_evar monotonous.Gravatar Pierre-Marie Pédrot2015-10-18
* Constraining refine to monotonic functions.Gravatar Pierre-Marie Pédrot2015-10-18
* Clarifying and documenting the UState API.Gravatar Pierre-Marie Pédrot2015-10-17
* Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-10-16
|\
| * Merge hint lists instead of appending them. (Fix bug #3199)Gravatar Guillaume Melquiond2015-10-16
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-15
|\|
| * Fixing perfomance issue of auto hints induced by universes.Gravatar Pierre-Marie Pédrot2015-10-14
| * Exporting the original unprocessed hint in the hint running function.Gravatar Pierre-Marie Pédrot2015-10-14
| * Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-12
|\|
| * Remove code that was already commented out.Gravatar Maxime Dénès2015-10-12
| * Fixing bug #4366: Conversion tactics recheck uselessly convertibility.Gravatar Pierre-Marie Pédrot2015-10-11
| * Fixing untimely unexpected warning "Collision between bound variables" (#4317).Gravatar Hugo Herbelin2015-10-11
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-10
|\|
| * Refine fix for handling of the universe contexts of hints, depending onGravatar Matthieu Sozeau2015-10-09
| * Fix CFGV contrib: handling of global hints introducing global universes.Gravatar Matthieu Sozeau2015-10-09
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-06
|\|
| * Fix bug #4354: interpret hints in the right env and sigma.Gravatar Matthieu Sozeau2015-10-06
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|\|
| * Univs: refined handling of assumptionsGravatar Matthieu Sozeau2015-10-02
| * Univs: fix evar_map handling in Hint processing.Gravatar Matthieu Sozeau2015-10-02
| * discriminate: Do fresh_global in the right env in presence of side-effects.Gravatar Matthieu Sozeau2015-10-02
| * Univs: fix many evar_map initializations and leaks.Gravatar Matthieu Sozeau2015-10-02
* | Removing uselessly duplicated function in Evd.Gravatar Pierre-Marie Pédrot2015-09-27
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-09-25
|\|
| * Hopefully better names to constructors of internal_flag, as discussedGravatar Hugo Herbelin2015-09-23
| * Give a way to control if the decidable-equality schemes are built likeGravatar Hugo Herbelin2015-09-23
| * Fixing bug #4207: setoid_rewrite creates self-referring hypotheses.Gravatar Pierre-Marie Pédrot2015-09-22
* | Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-09-17
|\|
| * In pat/constr introduction patterns, fixing in a better way clearing problemsGravatar Hugo Herbelin2015-09-16
| * Continuing investigation on how to preserve the locality of the actionGravatar Hugo Herbelin2015-09-16
| * Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
* | Merge remote-tracking branch 'origin/v8.5' into trunkGravatar Hugo Herbelin2015-09-09
|\|
| * Fixing incomplete bugfix in 76f27140e6e34 (unfortunately 5 commitsGravatar Hugo Herbelin2015-09-08
| * Ensuring that patterns of the form pat/constr move the hypotheses replacingGravatar Hugo Herbelin2015-09-08
| * Short cosmetic changes in tactics.ml.Gravatar Hugo Herbelin2015-09-08
| * A bit of documentation of OCaml code for intro_patterns.Gravatar Hugo Herbelin2015-09-08
| * New option "Unset Bracketing Last Introduction Pattern" for preservingGravatar Hugo Herbelin2015-09-08
| * Fixing clearing of temporary hypotheses with intro pattern pat/constr.Gravatar Hugo Herbelin2015-09-08
| * Fixing "pose proof (H ...) as H" and "assert (H:=H ...) which were supposedGravatar Hugo Herbelin2015-09-08
* | Allowing the abstract tactical to clear the environment from unused variables.Gravatar Pierre-Marie Pédrot2015-08-22
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-08-05
|\|
| * Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
| * Give a way to control if the decidable-equality schemes are built likeGravatar Hugo Herbelin2015-08-02
| * Granting Jason's request for an ad hoc compatibility option onGravatar Hugo Herbelin2015-08-02
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-07-29
|\|
| * Fix for bug #4280: "decide equality produces terms that don't compute well".Gravatar Pierre-Marie Pédrot2015-07-28
| * Fixing bug #3509 and #3510 (anomalies in "tactics/term_dnet.ml").Gravatar Pierre-Marie Pédrot2015-07-28