aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Collapse)AuthorAge
* Fix [Existing Class] impl and add documentation. Fix computation of theGravatar msozeau2010-02-10
| | | | | | | dependency order of obligations that was not backwards-compatible. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12719 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update CHANGES, add documentation for new commands/tactics and do a bitGravatar msozeau2010-01-30
| | | | | | | of cleanup in tactics/ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12705 85f007b7-540e-0410-9357-904b9bb8a0f7
* Support for generalized rewriting under dependent binders, using theGravatar msozeau2010-01-26
| | | | | | | [forall_relation] combinator. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12693 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quick fix for references to section variables unbound in the currentGravatar msozeau2010-01-26
| | | | | | | environment during unification. Should be checked earlier. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12692 85f007b7-540e-0410-9357-904b9bb8a0f7
* New version of 12650 that was broken (supporting again records whenGravatar herbelin2010-01-12
| | | | | | descending dependent conjunctions). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12658 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added module sharing support for typeclasses and hints (pri_auto_tactic).Gravatar soubiran2010-01-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12655 85f007b7-540e-0410-9357-904b9bb8a0f7
* revert commit 12650 for the moment, since it breaks MSetAVLGravatar letouzey2010-01-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12651 85f007b7-540e-0410-9357-904b9bb8a0f7
* Temporary fix to compensate the loss of descent on dependentGravatar herbelin2010-01-12
| | | | | | | | conjunctions (defined records now supported again but not unregistered ones). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12650 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2146 (broken selection of occurrences in "change").Gravatar herbelin2009-12-30
| | | | | | | | | | In trunk the different possible combinations of "at" and "in" with occurrences are taken into account. In 8.2 branch, it remains fragile (syntaxes that were accepted remain accepted and a message warns if the occurrences coming after the "with" are not taken into account). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12614 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improving descend_in_conjunctions (using a combinators instead of a tactic)Gravatar herbelin2009-12-29
| | | | | | | what allows to better control position of side-conditions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12612 85f007b7-540e-0410-9357-904b9bb8a0f7
* Safer, though ad hoc, approach to re-interpretation of the argument ofGravatar herbelin2009-12-28
| | | | | | | | | | | | | | | | | | general_multi_multi_rewrite. Due to the option "!" of rewrite, a lemma may need to be interpreted several times with different instances of the implicit arguments. Interpreting the term as a constr in tacinterp.ml would need to either refresh the holes (i.e. the evars) or detype what has been typed and in both cases, complicated things can happen because the evars associated to these holes may have been used in instantiating former evars of the goal. Leaving the term as a rawconstr would need to export the interpretation functions from tacinterp which is technically complicated in the current situation because equality.ml is currently linked before tacinterp. The solution used is to delay the interpretation using an ML closure. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12610 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix "Existing Instance" to handle globality information and "ExistingGravatar msozeau2009-12-27
| | | | | | | | | Class" too to handle references instead of just idents. Minor fix in coqdoc. zeta-normalize setoid_rewrite proofs, removing useless let-bindings generated by the tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12609 85f007b7-540e-0410-9357-904b9bb8a0f7
* In "simpl c" and "change c with d", c can be a pattern.Gravatar herbelin2009-12-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12608 85f007b7-540e-0410-9357-904b9bb8a0f7
* Opened the possibility to type Ltac patterns but it is not fully functional yetGravatar herbelin2009-12-24
| | | | | | | | | | | | | | | - to type patterns w/o losing the information of what subterm is a hole would need to remember where holes were in "understand", but "understand" needs sometimes to instantiate evars to ensure the type of an evar is not its original type but the type of its instance (what can e.g. lower a universe level); we would need here to update evars type at the same time we define them but this would need in turn to check the convertibility of the actual and expected type since otherwise type-checking constraints may disappear; - typing pattern is apparently expensive in time; is it worth to do it for the benefit of pattern-matching compilation and coercion insertion? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12607 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved a bit further the code for pattern interpretation in match goalGravatar herbelin2009-12-23
| | | | | | | | | to anticipate support of possibly-typed patterns; Also removed a useless nf_evar. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12606 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generic support for open terms in tacticsGravatar herbelin2009-12-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We renounced to distribute evars to constr and bindings and to let tactics do the merge. There are now two disciplines: - the general case is that the holes in tactic arguments are pushed to the general sigma of the goal so that tactics have no such low-level tclEVARS, Evd.merge, or check_evars to do: - what takes tclEVARS and check_evars in charge is now a new tactical of name tclWITHHOLES (this tactical has a flag to support tactics in either the "e"- mode and the non "e"- mode); - the merge of goal evars and holes is now done generically at interpretation time (in tacinterp) and as a side-effect it also anticipates the possibility to refer to evars of the goal in the arguments; - with this approach, we don't need such constr/open_constr or bindings/ebindings variants and we can get rid of all ugly inj_open-style coercions; - some tactics however needs to have the exact subset of holes known; this is the case e.g. of "rewrite !c" which morally reevaluates c at each new rewriting step; this kind of tactics still receive a specific sigma around their arguments and they have to merge evars and call tclWITHHOLES by themselves. Changes so that each specific tactics can take benefit of this generic support remain to be done. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12603 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack on making exact hints for lemmas starting with productsGravatar msozeau2009-12-19
| | | | | | | | (e.g. transitivity lemmas) and fix bug #2207, avoiding the generation of useless eta-redexes during type class instance resolution. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12600 85f007b7-540e-0410-9357-904b9bb8a0f7
* adding an option functional_induction_rewrite_dependent to make functional ↵Gravatar jforest2009-12-16
| | | | | | induction using not v8.2 version of subst. By default functional induction uses new version of subst git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12592 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved strategy for rewriting lemma possibly depending because of evars.Gravatar herbelin2009-12-14
| | | | | | | | Explained in CHANGES how to cope with the change of semantics of abbreviations wrt implicit arguments positions propagation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12586 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made the side-conditions of lemmas always come last when chaining "apply in"Gravatar herbelin2009-12-13
| | | | | | | in presence of destruction of conjunctive types. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12584 85f007b7-540e-0410-9357-904b9bb8a0f7
* Completion of r12580 (better rendering of dependent rewrite and inversion).Gravatar herbelin2009-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12583 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revision 12557 continued (better rendering of dependent rewrite)Gravatar herbelin2009-12-13
| | | | | | (expected goal was not correct for rewriting in hypotheses) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12580 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated compatibility for rewriting equality proofs that are dependentGravatar herbelin2009-12-12
| | | | | | | | | | - made the new "subst'" the default by renaming it "subst"; - renamed old "subst" into "simple subst"; - add option for non-rewriting of dependent proofs in general_rewrite and co - kept use of dependent proofs in the "subst" call of "functional induction", in spite it introduced incompatibilities (in Compcert). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12578 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved the rendering of "dependent rewrite" and hence of "inversion"Gravatar herbelin2009-12-12
| | | | | | by contracting in advance the projT (existT ...) redexes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12577 85f007b7-540e-0410-9357-904b9bb8a0f7
* Turn evars created by a tactic application into a subgoal immediately inGravatar msozeau2009-12-06
| | | | | | | | | typeclass resolution. Makes the backtracking heuristic correct again and avoids "late" backtracking on an unsolvable existential. Compilation time is back to normal. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12564 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix anomaly when using typeclass resolution with filtered hyps in evars.Gravatar msozeau2009-12-06
| | | | | | | | | | Make setoid_rewrite-through-rewrite's selection of occurences more robust: do not try unification with reduction if not needed. This changes a few scripts that were using reduction in a far from obvious way and could break more. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12562 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restored rewriting of JMeq using JMeq_rect and co when the domains are the sameGravatar herbelin2009-12-03
| | | | | | (this was lost since revision 12481). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12560 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix make_exact_entry to allow applying [forall x, P x] hints directly,Gravatar msozeau2009-12-01
| | | | | | | | | avoiding the introduction of eta-redexes. Prioritize hints over intros in typeclass resolution to profit from that. Add a minor fix in coqdoc by F. Garillot. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12550 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug in typeclass resolution. Better handling of universes inGravatar msozeau2009-12-01
| | | | | | | the generalization tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12548 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix backtracking heuristic in typeclass resolution. Gravatar msozeau2009-11-30
| | | | | | | | | | | | Now that backtracking is working correctly, we need to avoid a non-termination issue introduced by the [RelCompFun] definition in RelationPairs, by adding a [Measure] typeclass. It could be used to have a uniform notation for measures/interpretations in Numbers and be but in the interfaces too, only the mimimal change was implemented. Fix syntax change in test-suite scripts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12547 85f007b7-540e-0410-9357-904b9bb8a0f7
* Substitute terms for evars-as-goals as soon as they are solved inGravatar msozeau2009-11-27
| | | | | | | typeclass resolution. Fixes a bug reported by Eelis van der Weegen. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12545 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes in typeclasses, avoiding repeated evar normalizations.Gravatar msozeau2009-11-24
| | | | | | | | | | | Improve generalization by equalities tactic, now allowing to generalize an arbitrary application, e.g. in preparation for applying an elimination principle for a function. This adds a flag to generalize_dep so that it doesn't abstract the variable if it is defined, just introducing a let-in. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12541 85f007b7-540e-0410-9357-904b9bb8a0f7
* Lazier behaviour of [auto] when introducing hypothesis: query the hint db's ↵Gravatar puech2009-11-21
| | | | | | only when necessary. Hopefully should speed up [auto] a little. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12538 85f007b7-540e-0410-9357-904b9bb8a0f7
* Addendum to revision 12501.Gravatar herbelin2009-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12505 85f007b7-540e-0410-9357-904b9bb8a0f7
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12502 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtracking on the use of automatically generated schemes forGravatar herbelin2009-11-11
| | | | | | | | | "eq"-rewriting (a few contributions are still referring explicitly to eq_rect, eq_ind and co and the new mechanism, though working also for dependent rewriting, is not powerful enough in general wrt fixpoint guard to claim being uniformly better). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12501 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibility ocaml <= 3.09Gravatar herbelin2009-11-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12493 85f007b7-540e-0410-9357-904b9bb8a0f7
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12485 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quick fix for restoring a left-to-right rewriting lemma compatibleGravatar herbelin2009-11-09
| | | | | | | with the guard condition + typo in the generation of _rec schemes in the impredicative case. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12484 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Cleaning and uniformisation in command.ml: - For better modularity and better visibility, two files got isolated out of command.ml: - lemmas.ml is about starting and saving a proof - indschemes.ml is about declaring inductive schemes - Decomposition of the functions of command.ml into a functional part and the imperative part - Inductive schemes: - New architecture in ind_tables.ml for registering scheme builders, and for sharing and generating on demand inductive schemes - Adding new automatically generated equality schemes (file eqschemes.ml) - "_congr" for equality types (completing here commit 12273) - "_rew_forward" (similar to vernac-level eq_rect_r), "_rew_forward_dep", "_rew_backward" (similar to eq_rect), "_rew_backward_dep" for rewriting schemes (warning, rew_forward_dep cannot be stated following the standard Coq pattern for inductive types: "t=u" cannot be the last argument of the scheme) - "_case", "_case_nodep", "_case_dep" for case analysis schemes - Preliminary step towards discriminate and injection working on any equality-like type (e.g. eq_true) - Restating JMeq_congr under the canonical form of congruence schemes - Renamed "Set Equality Scheme" into "Set Equality Schemes" - Added "Set Rewriting Schemes", "Set Case Analysis Schemes" - Activation of the automatic generation of boolean equality lemmas - Partial debug and error messages improvements for the generation of boolean equality and decidable equality - Added schemes for making dependent rewrite working (unfortunately with not a fully satisfactory design - see file eqschemes.ml) - Some names of ML function made more regular (see dev/doc/changes.txt) - Incidentally, added a flush to obsolete Local/Global syntax warning git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12481 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fix discharge bug in typeclasses: some constrs were not actuallyGravatar msozeau2009-11-06
| | | | | | | | | discharged on the other definitions in the section. - Avoid universe problem in generalize_eqs were we could give an [@eq_refl Set x x] proof where an [@eq Type x x] was expected. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12478 85f007b7-540e-0410-9357-904b9bb8a0f7
* Misc fixes.Gravatar msozeau2009-11-06
| | | | | | | | | | | | | | - Correct backtracking function of coqdoc to handle the _p fields of lexers - Try a better typesetting of [[ ]] inline code considering it as blocks and not purely inline code like [ ] escapings. - Rework latex macros for better factorization and support external references in pdf output. - Better criterion for generalization of variables in dependent elimination tactic and better error message in [specialize_hypothesis]. - In autounfold, don't put the core unfolds by default. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12474 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.Gravatar gmelquio2009-11-04
| | | | | | | Fixed pretty printing of record syntax. Allowed record syntax inside patterns. (Patch by Cedric Auger.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12468 85f007b7-540e-0410-9357-904b9bb8a0f7
* Integrate a few improvements on typeclasses and Program from the equations ↵Gravatar msozeau2009-10-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | branch and remove equations stuff which moves to a separate plugin. Classes: - Ability to define classes post-hoc from constants or inductive types. - Correctly rebuild the hint database associated to local hypotheses when they are changed by a [Hint Extern] in typeclass resolution. Tactics and proofs: - Change [revert] so that it keeps let-ins (but not [generalize]). - Various improvements to the [generalize_eqs] tactic to make it more robust and produce the smallest proof terms possible. Move [specialize_hypothesis] in tactics.ml as it goes hand in hand with [generalize_eqs]. - A few new general purpose tactics in Program.Tactics like [revert_until] - Make transitive closure well-foundedness proofs transparent. - More uniform testing for metas/evars in pretyping/unification.ml (might introduce a few changes in the contribs). Program: - Better sorting of dependencies in obligations. - Ability to start a Program definition from just a type and no obligations, automatically adding an obligation for this type. - In compilation of Program's well-founded definitions, make the functional a separate definition for easier reasoning. - Add a hint database for every Program populated by [Hint Unfold]s for every defined obligation constant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12440 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clarification in commentsGravatar glondu2009-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12437 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove old compatibility stuff (Tacred.nf)Gravatar glondu2009-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12436 85f007b7-540e-0410-9357-904b9bb8a0f7
* Make usage of Dyn explicitGravatar glondu2009-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12435 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backport fix for indexing of sorts which collapse every Type occurrenceGravatar msozeau2009-10-28
| | | | | | | into a SortLabel None. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12434 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes around typeclasses:Gravatar msozeau2009-10-27
| | | | | | | | | | | | | | - Correct discharge/classify/rebuild for instances. Semantic of Global/Local: local by default in sections, global by default in modules. - Fix the discrimination net's handling of type universes, let the unification do it. - Correct the typeclass resolution tactic so that when extern tactics themselves launch class resolution we don't duplicate work. Problem reported by Arthur Chargueraud. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12427 85f007b7-540e-0410-9357-904b9bb8a0f7
* fix previous commitGravatar corbinea2009-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12424 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 13:14:24 +0000