aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Revert "Improve the interpretation scope of arguments of an ltac match."Gravatar Maxime Dénès2016-07-04
* Fixing use of "Declare Implicit Tactic" in refine.Gravatar Hugo Herbelin2016-07-01
* Fixing #4881 (synchronizing "Declare Implicit Tactic" with backtrack).Gravatar Hugo Herbelin2016-07-01
* Merge branch 'bug4450' into v8.5Gravatar Matthieu Sozeau2016-06-14
|\
* | Fixing a try with in apply that has become too weak in 8.5.Gravatar Hugo Herbelin2016-06-11
* | Improve the interpretation scope of arguments of an ltac match.Gravatar Hugo Herbelin2016-06-09
| * Univs/(e)auto: fix bug #4450 polymorphic exact hintsGravatar Matthieu Sozeau2016-06-09
|/
* Revert "Rename Lexer -> CLexer."Gravatar Pierre-Marie Pédrot2016-05-31
* Fix bug #4746: Anomaly: Evar ?X10 was not declared.Gravatar Pierre-Marie Pédrot2016-05-29
* rewrite/Univs: Fix bug # 4498.Gravatar Matthieu Sozeau2016-05-26
* Hints/Univs: fix bug #4628 anomaliesGravatar Matthieu Sozeau2016-05-23
* Rename Lexer -> CLexer.Gravatar Pierre-Marie Pédrot2016-05-09
* In Regular Subst Tactic mode, ensure that the order of hypotheses isGravatar Hugo Herbelin2016-05-03
* Fix bug #4707: clearbody much slower in 8.5pl1.Gravatar Pierre-Marie Pédrot2016-05-03
* Allow to unset the refinement mode of Instance in MLGravatar Matthieu Sozeau2016-04-07
* Fixing an incorrect use of prod_appvect on a term which was not aGravatar Hugo Herbelin2016-04-07
* Fixing the "No applicable tactic" non informative error messageGravatar Hugo Herbelin2016-04-03
* Fixing bug #4630: Some tactics are 20x slower in 8.5 than 8.4.Gravatar Pierre-Marie Pédrot2016-03-20
* Fix strategy of Keyed UnificationGravatar Matthieu Sozeau2016-03-09
* Fixing bug #4596: [rewrite] broke in the past few weeks.Gravatar Pierre-Marie Pédrot2016-02-28
* Fix bug #4544: Backtrack on using full betaiota reduction during keyed unific...Gravatar Matthieu Sozeau2016-02-23
* Fix regression from 8.4 in reflexivity/...Gravatar Matthieu Sozeau2016-02-19
* Fix bug #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity").Gravatar Pierre-Marie Pédrot2016-02-17
* Fix bug #4537: Coq 8.5 is slower in typeclass resolution.Gravatar Pierre-Marie Pédrot2016-01-27
* Fixing bug #4511: evar tactic can create non-typed evars.Gravatar Pierre-Marie Pédrot2016-01-24
* Implement support for universe binder lists in Instance and Program Fixpoint/...Gravatar Matthieu Sozeau2016-01-23
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Fix bug #4420: check_types was losing universe constraints.Gravatar Matthieu Sozeau2016-01-19
* Fix essential bug in new Keyed Unification mode reported by R. Krebbers.Gravatar Matthieu Sozeau2016-01-12
* Fix bug #3338 again, no progress is necessary for the success of rewrite_strat.Gravatar Matthieu Sozeau2016-01-11
* Fix bug #4480: progress was not checked for setoid_rewrite.Gravatar Matthieu Sozeau2016-01-07
* FIx parsing of tactic "simple refine".Gravatar Maxime Dénès2015-12-16
* Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".Gravatar Guillaume Melquiond2015-12-16
* Refine tactic now shelves unifiable holes.Gravatar Pierre-Marie Pédrot2015-12-15
* Changing the order of the goals generated by unshelve.Gravatar Pierre-Marie Pédrot2015-12-15
* Add tactic native_cast_no_check, analog to vm_cast_no_check.Gravatar Maxime Dénès2015-12-11
* Fixing a pat%constr bug. Thanks to Enrico for reporting.Gravatar Hugo Herbelin2015-12-10
* Silently ignore requests to _not_ clear something when that something cannot ...Gravatar Guillaume Melquiond2015-12-10
* Fixing parsing of the unshelve tactical.Gravatar Pierre-Marie Pédrot2015-12-09
* Adding an unshelve tactical.Gravatar Pierre-Marie Pédrot2015-12-09
* Fix some typos.Gravatar Guillaume Melquiond2015-12-07
* Fix in setoid_rewrite in Type: avoid the generation of a rigid universeGravatar Matthieu Sozeau2015-12-04
* 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
* Fix [Polymorphic Hint Rewrite].Gravatar Matthieu Sozeau2015-11-27
* Fix generation of equality schemes on polymorphic equality types.Gravatar Matthieu Sozeau2015-11-23
* Fix bug #4429: eauto with arith: 70x performance regression in Coq 8.5.Gravatar Pierre-Marie Pédrot2015-11-19
* Fix bug #4433, removing hack on evars appearing in a pattern from aGravatar Matthieu Sozeau2015-11-19
* Improve error message.Gravatar Maxime Dénès2015-11-18
* More optimizations of [Clenv.clenv_fchain].Gravatar Pierre-Marie Pédrot2015-11-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 02:59:03 +0000