aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Collapse)Author
2010-02-10ajout test de fied_simplify_eq inbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12730 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-12New version of 12650 that was broken (supporting again records whenherbelin
descending dependent conjunctions). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12658 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-12revert commit 12650 for the moment, since it breaks MSetAVLletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12651 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-12Temporary fix to compensate the loss of descent on dependentherbelin
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
2010-01-04Errors issued by reduction tactics (e.g. pattern) were not caught by "try".herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12621 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-30Fixing bug #2146 (broken selection of occurrences in "change").herbelin
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
2009-12-29Renouncing to have the option "Automatic Introduction" on by default.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12613 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-29Improving descend_in_conjunctions (using a combinators instead of a tactic)herbelin
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
2009-12-24In "simpl c" and "change c with d", c can be a pattern.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12608 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-13Made the side-conditions of lemmas always come last when chaining "apply in"herbelin
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
2009-12-13Revision 12557 continued (better rendering of dependent rewrite)herbelin
(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
2009-11-30Fix backtracking heuristic in typeclass resolution. msozeau
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
2009-11-27Added support for definition of fixpoints using tactics.herbelin
Fixed some bugs in -beautify and robustness of {struct} clause. Note: I tried to make the Automatic Introduction mode on by default for version >= 8.3 but it is to complicated to adapt even in the standard library. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12546 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-27Substitute terms for evars-as-goals as soon as they are solved inmsozeau
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
2009-11-13Fix test-suite scripts: [Generalizable Variables] and small msozeau
changes in obligations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12514 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-11Test for bug #2168, forgotten in r12496.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12497 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-11Improving abbreviations/notations + backtrack of semantic change in r12439herbelin
- Deactivation of short names registration and printing for abbreviations to identical names, what avoids printing uselessly qualified names binding where the short name is in fact equivalent. - New treatment of abbreviations to names: don't insert any maximally inserted implicit arguments at all at the time of the abbreviation and use the regular internalization strategy to have them inserted at use time. - The previous modifications altogether make redirections of qualified names easier and avoid the semantic change of r12349 and hence allows to keep "Notation b := @a" as it was before, i.e. as a notation for the deactivation of the implicit arguments of a. - Took benefit of these changes and updated nil/cons/list/app redefinition in "List.v". - Fixed parsing/printing notation bugs (loop on partially applied abreviations for constructors in constrintern.ml + bad reverting of notations with holes that captured non anonymous variables in match_cases_pattern). - Add support for parsing/printing abbreviations to @-like constructors and for reverting printing for abbreviations to constructors applied to parameters only (function extern_symbol_pattern). - Minor error messages fixes and minor APIs cleaning. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12494 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
- 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
2009-10-30Attempt to capture on time unification errors for "with" bindings.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12450 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-29Revision 12439 continued, printing part (notations to names behaveherbelin
like the name they refer to). Fixing buggy test-suite implicit.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12442 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-28Integrate a few improvements on typeclasses and Program from the equations ↵msozeau
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
2009-10-28Made that notations to names behave like the names they refer to wrtherbelin
implicit arguments and scope (use Implicit Arguments or Arguments Scope commands instead if not the desired behaviour). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12439 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-26Local/Global revision 12418 continuedherbelin
- Fixing non-export of newly created Local Argument Scope. - Fixing bad discharge of local variables in nested sections (bug still exists in v8.2). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12420 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-26Adapted test unfold.v after eq gets its argument maximally insertedherbelin
(commit r12379). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12419 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-25Restore (and test) broken chaining of lemmas in "apply in" in presenceherbelin
of side conditions. Fix a small presentation issue in printing the "exists" tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12416 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-25Add support for remaining side-conditions in "apply in as".herbelin
Tolerate that the place where to move an hypothesis with destruct is not "safe" if the lemma has dependent parameters inferred lately. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12412 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-25Improved the treatment of Local/Global options (noneffective Local onherbelin
Implicit Arguments, Arguments Scope and Coercion fixed, noneffective Global in sections for Hints and Notation detected). Misc. improvements (comments + interpretation of Hint Constructors + dev printer for hint_db). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12411 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-17Fixed a notation bug when extending binder_constr with empty levelsherbelin
(see Notations.v). Improved the "already occurs in a different scope" test and message. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12399 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-04Removal of trailing spaces.serpyc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12371 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-27Fixed a bug in the interaction between dEqThen and inject_at_positionsherbelin
which was disturbing inversion and sometimes making it failing in presence of dependent equalities (injection still doesn't know how to split dependent equalities, resulting in a smaller number of equalities than expected for dEqThen). [also restored inv.ml as it was before 12356 which uselessly and inadvertently modified it] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12360 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-27Fixed two tests that was incorrectly typed in former revisions 12348 and 12356.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12359 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-27Delay the choice of eliminator in destruct/induction until we know ifherbelin
a dependent scheme is needed or not (this allows for instance "destruct H" when H is propositional and dependent in the context to work). Modest attempt to clarify the basic components used and invariants preserved when sharing the code for functional induction and for destruct/induction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12356 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-22Add the option to automatically introduce variables declared before themsozeau
colon in (mutual) proofs with [Set Automatic Introduction]. Fix a minor test-suite issue in ProgramWf due to new handling of the default obligation tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12351 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-20Only one "in" clause in "destruct" even for a multiple "destruct".herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12348 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-11Ensures that let-in's in arities of inductive types work well. Maybe notherbelin
very useful in practice but as soon as let-in's were not forbidden in the internal data structure, better to do it. Moreover, this gets closer to the view were inductive definitions are uniformly built from "contexts". (checker not changed!) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12273 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-20Move some examples for groebner into a test-suite fileletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12244 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-15- Granted wish #2138 (support for local binders in syntax of Record fields).herbelin
- Add tests related to commits 12229 (bug #2117) and 12241 (bug #2139). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12242 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-08Reactivation of pattern unification of evars in apply unification, inherbelin
agreement with wish #2117 (pattern unification of evars remained deactivated for 3 years because of incompatibilities with eauto [see commit 9234]; thanks to unification flags, it can be activated for apply w/o changing eauto). Also add test for bug #2123 (see commit 12228). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12229 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-06Fixing bug #2106 ("match" compilation with multi-dependent constructor).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12167 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-02Adding a regression test about Bauer's example on coq-club ofherbelin
rewriting using eta. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12161 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-02Fix script file using the "Manual Implicit" flag.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12158 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-10- Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: itherbelin
revealed a too strict test for detection of inferable metas in Clenv. Restored tolerance for unbound names in interactive tactic use. - Moral removals of some captures of Not_found in Environ.evaluable_* since kernel is assumed to deal with existing names. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12122 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-25- Fixing #2090 (occur check missing when trying to solve evar-evar equation).herbelin
- Adding test file related to commit 12080 (bug #2091). - Cleaning old parsing stuff from 8.0. - Support for camlp5 in base_include. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12106 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-10Fix premature optimisation in dependent induction: even variable args needmsozeau
to be generalized as they may appear in other arguments or their types. Try to keep the original names around as well, using the ones found in the goal. This only requires that interning a pattern [forall x, _] properly declares [x] as a metavariable, binding instances are already part of the substitutions computed by [extended_matches]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12079 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-08- Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixingherbelin
Not_found bug in Theorem with) from V8.2 to trunk. - Improving indentation in presence of tabulation and utf-8 when reporting error messages with "^^^^^^". - Updating a few svn:ignore properties. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12059 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-29Avoid inadvertent declaration of "on" as a keyword. New syntax ismsozeau
{measure ms [id] [(rel)]}. Fix script of bug #2083 and test-suite file accordingly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12032 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-28Rewrite of Program Fixpoint to overcome the previous limitations: msozeau
- The measure can now refer to all the formal arguments - The recursive calls can make all the arguments vary as well - Generalized to any relation and measure (new syntax {measure m on R}) This relies on an automatic curryfication transformation, the real fixpoint combinator is working on a sigma type of the arguments. Reduces to the previous impl in case only one argument is involved. The patch also introduces a new flag on implicit arguments that says if the argument has to be infered (default) or can be turned into a subgoal/obligation. Comes with a test-suite file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12030 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-19coq_makefile: -c and -shared conflict; tacinterp: delay evaluation of tactic ↵barras
genargs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11995 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-16Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"herbelin
now works correctly, "unfold foo at 4 in H at 3" now fails correctly, etc.). The terminology for clauses (though I don't find the term "clause" very intuitive after all) is mostly preserved except for "simple_clause" which becomes a light form of "clause" instead of being an atom of clause (what played the role of "simple_clause" is now called "goal_location" - better names are welcome). Main changes are in tacticals.ml and tactics.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11981 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-16 00:13:04 +0000