aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.ml
Commit message (Expand)AuthorAge
...
| * Fix bug #4151: discrepancy between exact and eexact/eassumption.Gravatar Matthieu Sozeau2015-11-02
* | Monotonizing Tactics.change_arg.Gravatar Pierre-Marie Pédrot2015-10-29
* | Removing the evar_map argument from s_enter.Gravatar Pierre-Marie Pédrot2015-10-29
* | Removing some goal unsafeness in inductive schemes.Gravatar Pierre-Marie Pédrot2015-10-29
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-29
|\|
| * 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
* | Proofview.Goal.sigma returns an indexed evarmap.Gravatar Pierre-Marie Pédrot2015-10-20
* | Boxing the Goal.enter primitive into a record type.Gravatar Pierre-Marie Pédrot2015-10-20
* | Renaming Goal.enter field into s_enter.Gravatar Pierre-Marie Pédrot2015-10-20
* | Expliciting the uses of the old Tacmach API in Tactics.Gravatar Pierre-Marie Pédrot2015-10-19
* | Removing some unsafe uses of monotonicity.Gravatar Pierre-Marie Pédrot2015-10-19
* | Type delayed_open_constr is now monotonic.Gravatar Pierre-Marie Pédrot2015-10-19
* | More monotonicity in Tactics.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
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-12
|\|
| * Fixing bug #4366: Conversion tactics recheck uselessly convertibility.Gravatar Pierre-Marie Pédrot2015-10-11
* | 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
* | 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
* | 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
|/
* Granting Jason's request for an ad hoc compatibility option onGravatar Hugo Herbelin2015-08-02
* Fixing bug #2814: "Anomaly: Uncaught exception Option.IsNone".Gravatar Pierre-Marie Pédrot2015-05-16
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Code simplification in Tactics.Gravatar Pierre-Marie Pédrot2015-05-04
* Cleaning some uses of exceptions in tactics.Gravatar Pierre-Marie Pédrot2015-04-25
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Using tclZEROMSG instead of tclZERO in several places.Gravatar Pierre-Marie Pédrot2015-04-23
* Fix #3590 for good this time, by changing the API, change's argument nowGravatar Matthieu Sozeau2015-04-10
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* Hack so that refine_no_check accepts an argument which is a match on anGravatar Hugo Herbelin2015-02-27
* Fixing printing of ordinals.Gravatar Pierre-Marie Pédrot2015-02-26
* Fixing error message when H already exists in tactic subexpression eqn:H.Gravatar Hugo Herbelin2015-02-20
* A fix for #3993 (not fully applied term to destruct when eqn is given).Gravatar Hugo Herbelin2015-02-20
* Univs: fix bug #4031: wrong folding of sigma in change.Gravatar Matthieu Sozeau2015-02-12
* Missing space in error messageGravatar Matěj Grabovský2015-02-11
* Fixing #4018 (uncaught exception on non-equality in intros [=]).Gravatar Hugo Herbelin2015-02-10
* More expressive API for tclWITHHOLES.Gravatar Pierre-Marie Pédrot2015-02-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 04:01:59 +0000