aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
2015-12-18Tying the loop in tactic printing API.Pierre-Marie Pédrot
2015-12-17Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-17Getting rid of some hardwired generic arguments.Pierre-Marie Pédrot
2015-12-16FIx parsing of tactic "simple refine".Maxime Dénès
2015-12-16Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".Guillaume Melquiond
2015-12-15Refine tactic now shelves unifiable holes.Pierre-Marie Pédrot
The unshelve tactical can be used to get the shelved holes. This changes the proper ordering of holes though, so expect some broken scripts. Also, the test-suite is not fixed yet.
2015-12-15Changing the order of the goals generated by unshelve.Pierre-Marie Pédrot
2015-12-15Granting clear_flag in injection, even legacy mode. This is possibleHugo Herbelin
since the clear_flag is new.
2015-12-13More code sharing between tactic notation and genarg interpretation.Pierre-Marie Pédrot
2015-12-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-11Add tactic native_cast_no_check, analog to vm_cast_no_check.Maxime Dénès
2015-12-10Fixing a pat%constr bug. Thanks to Enrico for reporting.Hugo Herbelin
2015-12-10Silently ignore requests to _not_ clear something when that something cannot ↵Guillaume Melquiond
be cleared. This should fix the contrib failures on tactics like "destruct (0)".
2015-12-09Fixing parsing of the unshelve tactical.Pierre-Marie Pédrot
Now [unshelve tac1; tac2] is parsed as [(unshelve tac1); tac2].
2015-12-09Adding an unshelve tactical.Pierre-Marie Pédrot
This tactical is inspired by discussions on the Coq-club list. For now it is still undocumented, and there is room left for design issues.
2015-12-08Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-07Fix some typos.Guillaume Melquiond
2015-12-05Fixing compilation with old CAMLPX versions.Pierre-Marie Pédrot
2015-12-05Removing redundant versions of generalize.Hugo Herbelin
2015-12-05Moving extended_rel_vect/extended_rel_list to the kernel.Hugo Herbelin
It will later be used to fix a bug and improve some code. Interestingly, there were a redundant semantic equivalent to extended_rel_list in the kernel called local_rels, and another private copy of extended_rel_list in exactly the same file.
2015-12-05Experimenting removing strong normalization of the mid-statement in tactic cut.Hugo Herbelin
2015-12-05Moving three related small half-general half-ad-hoc utility functionsHugo Herbelin
next to each other, waiting for possible integration into a more uniform API.
2015-12-05Getting rid of some quoted tactics in Tauto.Pierre-Marie Pédrot
2015-12-04Getting rid of the dynamic node of the tactic AST.Pierre-Marie Pédrot
2015-12-04Fix in setoid_rewrite in Type: avoid the generation of a rigid universeMatthieu Sozeau
on applications of inverse (flip) on a crelation. This was poluting universe constraints of lemmas using generalized rewriting in Type.
2015-12-04Removing the last use of valueIn in Tauto.Pierre-Marie Pédrot
2015-12-04Removing dynamic inclusion of constrs in tactic AST.Pierre-Marie Pédrot
2015-12-03Removing the globTacticIn primitive.Pierre-Marie Pédrot
It was not used in Coq codebase, and the only known user was ssreflect up to commit 95354e0dee.
2015-12-03Fixing Tauto compilation for older versions of OCaml.Pierre-Marie Pédrot
2015-12-03Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-03Removing the last use of tacticIn in setoid_ring.Pierre-Marie Pédrot
2015-12-03Removing the use of tacticIn in Tauto.Pierre-Marie Pédrot
2015-12-02Slight simplification of code for pat/constr.Hugo Herbelin
2015-12-02Dead code from August 2014 in apply in.Hugo Herbelin
2015-12-02Removing dead code in Obligations.Pierre-Marie Pédrot
2015-11-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-27Fix [Polymorphic Hint Rewrite].Matthieu Sozeau
2015-11-26Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-23Fix generation of equality schemes on polymorphic equality types.Matthieu Sozeau
2015-11-23Removing a use of old refine in Tactics.Pierre-Marie Pédrot
2015-11-20Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-19Fix bug #4429: eauto with arith: 70x performance regression in Coq 8.5.Pierre-Marie Pédrot
The issue was due to the fact that unfold hints are given a priority of 4 by default. As eauto was now using hint priority rather than the number of goals produced to order the application of hints, unfold were almost always used too late. We fixed this by manually giving them a priority of 1 in the eauto tactic. Also fixed the relative order of proof depth w.r.t. hint priority. It should not be observable except for breadth-first search, which is seldom used.
2015-11-19Fix bug #4433, removing hack on evars appearing in a pattern from aMatthieu Sozeau
constr, and the associated signature, not needed anymore. Update CHANGES, no evar_map is produced by pattern_of_constr anymore.
2015-11-18Improve error message.Maxime Dénès
2015-11-18Inlining the only use of Clenv.connect_clenv.Pierre-Marie Pédrot
2015-11-17More optimizations of [Clenv.clenv_fchain].Pierre-Marie Pédrot
Everywhere we know that the universes of the left argument are an extension of the right argument, we do not have to merge universes.
2015-11-17Performance fix for destruct.Pierre-Marie Pédrot
The clenv_fchain function was needlessly merging universes coming from two evarmaps even though one was an extension of the other. A flag was added so that the tactic just retrieves the newer universes.
2015-11-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-13Continue fix of PMP, handling setoid_rewrite in let-bound hyps correctly.Matthieu Sozeau
2015-11-11Fix bug #3257, setoid_reflexivity should fail if not completing the goal.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 00:45:23 +0000