aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* More optimizations of [Clenv.clenv_fchain].Gravatar Pierre-Marie Pédrot2015-11-17
* Performance fix for destruct.Gravatar Pierre-Marie Pédrot2015-11-17
* Continue fix of PMP, handling setoid_rewrite in let-bound hyps correctly.Gravatar Matthieu Sozeau2015-11-13
* Fix bug #3257, setoid_reflexivity should fail if not completing the goal.Gravatar Matthieu Sozeau2015-11-11
* Typo.Gravatar Hugo Herbelin2015-11-10
* Fix bug #4404: [remember] gives Error: Conversion test raised an anomaly.Gravatar Pierre-Marie Pédrot2015-11-10
* Preservation of the name of evars/goals when applying pose/set/intro/clearbody.Gravatar Hugo Herbelin2015-11-07
* Fix bug #4273Gravatar Matthieu Sozeau2015-11-05
* Hint Cut documentation and cleanup of printing (was duplicated andGravatar Matthieu Sozeau2015-11-04
* Fix bug in proofs/logic.ml type_of_global_reference_knowing_conclusionGravatar Matthieu Sozeau2015-11-04
* Fix bug #4397: refreshing types in abstract_generalize.Gravatar Matthieu Sozeau2015-11-02
* Fix bug #4151: discrepancy between exact and eexact/eassumption.Gravatar Matthieu Sozeau2015-11-02
* Avoid an anomaly when destructing an unknown ident. (Fix bug #4395)Gravatar Guillaume Melquiond2015-10-29
* Fixing another instance of bug #3267 in eauto, this time in theGravatar Hugo Herbelin2015-10-29
* Univs: local names handling.Gravatar Matthieu Sozeau2015-10-28
* Avoid type checking private_constants (side_eff) again during Qed (#4357).Gravatar Enrico Tassi2015-10-28
* Preserving goal name in revert/bring_hyps.Gravatar Hugo Herbelin2015-10-26
* Fixing a loop in checking hints with holes.Gravatar Hugo Herbelin2015-10-24
* Backtracking on interpreting toplevel calls to exact in scope determinedGravatar Hugo Herbelin2015-10-24
* Categorizing debug messages as such + NonLogical uses loggers.Gravatar Pierre Courtieu2015-10-19
* Turning anomaly into error for #4372 (weakness of inversion in theGravatar Hugo Herbelin2015-10-19
* Generalize fix for auto from PMP to eauto and typeclasses eauto.Gravatar Matthieu Sozeau2015-10-16
* Merge hint lists instead of appending them. (Fix bug #3199)Gravatar Guillaume Melquiond2015-10-16
* 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
* 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
* 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
* Fix bug #4354: interpret hints in the right env and sigma.Gravatar Matthieu Sozeau2015-10-06
* 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
* 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
* 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
* 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
* Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 08:39:42 +0000