-
Notifications
You must be signed in to change notification settings - Fork 110
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
"elim/v: t" weaker than "elim t using v" #2
Labels
kind: bug
Issue which describe bugs
Comments
gares
pushed a commit
that referenced
this issue
Sep 10, 2015
Also: - fix elim trying to saturate too much and not raising the expected exn - fix fill_occ_pattern when occ is {-}, it used to lose the instantiation obtained by matching the term
This should be fixed by 33d9a59 on the feature/plugin-next branch |
gares
pushed a commit
that referenced
this issue
Dec 3, 2015
Also: - fix elim trying to saturate too much and not raising the expected exn - fix fill_occ_pattern when occ is {-}, it used to lose the instantiation obtained by matching the term
gares
pushed a commit
that referenced
this issue
Dec 11, 2015
fd85f1e html doc generated a6f22db coqdoc + interactive graph browsing REVERT: 1baf306 html doc generated REVERT: bb4f01d link in the root directory README, INSTALL, ... REVERT: 2042765 removing files not in mathcomp-1.6 REVERT: 353eb61 coqdoc + interactive graph browsing REVERT: f943e8d 8.5 coqdoc does not want _ to be escaped + more .css classes REVERT: 006565b HACK: work around regression in 8.5 REVERT: 80b5cea some doc for the doc building utility REVERT: e5babdb Updated the address of the website in README REVERT: 2291fa4 Moved comments on the incompatibility to INSTALL. REVERT: 6f88b1d Create ANNOUNCE-github.md REVERT: 5c64366 update license banner in .ml files REVERT: c3cd260 Trying a better layout of hyperlinks on github REVERT: 2e15ff9 Trying a better layout of the .md on github REVERT: 8780445 Minor edition of the Announce. REVERT: 9adb947 Update ANNOUNCE-1.6.md REVERT: 672865b Merge branch 'master' of https://github.com/math-comp/math-comp REVERT: 732a8c3 Trailing whitespace removal REVERT: e22704b Ignore emacs checkpoints REVERT: 19ac062 Remove spurious injections REVERT: 03363b8 Explicit construction of finite fields REVERT: bafc4ee Some proof refactoring REVERT: 37f0673 Move finfield to field module REVERT: 058ec3b Add elementary abelian finite modules lemmas to abelian REVERT: 8318a82 Remove spurious injections REVERT: efc830f Add instances & lemmas for regular algebras REVERT: bd8cf1b Document limitation of fieldExtType cloning REVERT: 903a5e4 Correct improper CS declaration REVERT: a2b30aa Add finLmodType, finLalgType and finAlgType instances REVERT: 7737563 Removed spurious injection & clean up proof REVERT: 0b22709 Remove more redundant power type structures REVERT: 12ee0cf Correct join values to baseFingroupType REVERT: 70073eb Remove redundant structures for finite powers REVERT: 8a5defa Add missing export REVERT: e6076b2 fix coq-mathcomp-ssreflect opam package description REVERT: 0b02d10 better wording and package description in the ANNOUNCE for 1.6 REVERT: cfb8011 some work on installation instructions and annoucement message REVERT: 95354e0 Removing the only use of globTacticIn. REVERT: 7bf7dca add .mailmap to uniform names/email of committers REVERT: 1e388e3 fix compilation on trunk (thanks PMP) REVERT: c570d3d fix: autogen + abstract variables clash REVERT: 4d0f111 fix: elim/v handles eliminator from Derive Inversion (issue #2) REVERT: 55a5aaa Add commands to trace the matching algorithm REVERT: de9aafb fix: Hint View is not a Query REVERT: 2d032b5 Typos in comments. REVERT: 986f8d6 Tested the Qed of the alternate Xirredp_FAdjoin in Coq 8.4. REVERT: fb82de6 Typo. REVERT: c084774 Typos REVERT: da9bec4 fix INSTALL symlinks REVERT: c5fd978 Adding sections for definitions in change log REVERT: 490d8fa Update ChangeLog REVERT: ec504e2 ChangeLog: yake Yves' suggestion into account REVERT: 1058783 First stab at INSTALL REVERT: 6862e60 basic has disappeared REVERT: 98cfa7e Makefile to create a tar ball REVERT: 57b0dfb Changelog file created REVERT: eb65b7b Update .git* conf files to ignore/exclude cruft REVERT: 14c9a3a merge basic/ into ssreflect/ REVERT: 35124d2 Added support for highlighting 'isn't' in PG. REVERT: 254379d Added suport for highlighting gen(erally) have in PG. REVERT: 00643ca Small updates in the documentation of the customization of PG. REVERT: 6275cbd Restaured the config files (including doc) for PG in the ssreflect package. REVERT: b0e32f6 fix compilation on trunk REVERT: 39cc672 Fix compilation on 8.5 REVERT: ade7c12 Fix typo in README. REVERT: 14c940b Compare pattern heads (constants) up to "univs" REVERT: e9163a8 fix trunk compilation REVERT: d4deb12 Update README.md REVERT: 29a193a fix PF REVERT: 1e448cd add a missing From ... REVERT: a0d8980 Update README.md REVERT: 8e787d8 First stab at the README (displayed on github) REVERT: 627a555 fix Makefiles REVERT: 5ac5791 fix path of Makefile.coq-makefile REVERT: cd072f4 update copyright banner REVERT: 2e6d512 factor common Makefile stuff REVERT: ab80631 Add a From ... REVERT: 5558b68 next blind fix REVERT: 4a1a55b blind fix REVERT: f538fc0 blind patch by Enrico REVERT: ab387ba forgotten import REVERT: 32e4af5 remove duplicate fields REVERT: adc15de opam meta-data +url REVERT: 8047173 make the opam package meta data REVERT: 6d3dcee make opam meta-data REVERT: 663721c update opam meta-data REVERT: 7f7f8b1 keeping track of the changes for trunk (import from svn) REVERT: 152decf fix Makefile for trunk REVERT: d410a44 patch ssrcoqdep REVERT: 40021d4 update to preserve backward compatibility with v8.4 REVERT: 532de9b Updating files + reorganizing everything REVERT: f180c53 character for v8.5 REVERT: 2a89801 field for v8.5 REVERT: 999e5fd adapting solvable to 8.5 REVERT: c8b1f98 packaging odd_order REVERT: 634ee87 Using the From X Require Y for v8.4 REVERT: 1681e3b support for camlp4 REVERT: 0284fa8 Forward compatibility with "From X Require Y." REVERT: de1794e packaging for v8.5 REVERT: 858957a packaging for v8.5 REVERT: 737f79e makefiles that are version dependent REVERT: abe2354 Makefile, testing for v8.5 and uncommenting stuff REVERT: 9fa572c prepared discrete for compilation in v8.5 REVERT: 9859058 Merge pull request #1 from mattam82/master REVERT: 244e554 Fix Makefiles. REVERT: 22d788f fix gitignore REVERT: 9335bfa support both coq.8.5beta1 and coq.8.5.dev REVERT: 54d0e3b plugin that compiles with 8.5 REVERT: 4633066 The right way to ignore the plugin directory REVERT: e2530e7 Broken global Makefile REVERT: d226438 packaging all REVERT: 086f066 character packaged REVERT: 821071c packaging real_closed REVERT: f3671d3 change finfield from field to character REVERT: c7ddacd metadata for solvable and field REVERT: 0d2a1e7 packaging fingroup and algebra REVERT: 0c07923 remove undo files REVERT: 155e671 some work on ssreflect and discrete REVERT: fc84c27 Initial commit git-subtree-dir: htmldoc git-subtree-split: fd85f1e3cb9a1cc05e8a6e6da7d65eebd4322c92
gares
pushed a commit
that referenced
this issue
May 9, 2016
d7a61bb html doc generated a6f22db coqdoc + interactive graph browsing REVERT: 1baf306 html doc generated REVERT: bb4f01d link in the root directory README, INSTALL, ... REVERT: 2042765 removing files not in mathcomp-1.6 REVERT: 353eb61 coqdoc + interactive graph browsing REVERT: f943e8d 8.5 coqdoc does not want _ to be escaped + more .css classes REVERT: 006565b HACK: work around regression in 8.5 REVERT: 80b5cea some doc for the doc building utility REVERT: e5babdb Updated the address of the website in README REVERT: 2291fa4 Moved comments on the incompatibility to INSTALL. REVERT: 6f88b1d Create ANNOUNCE-github.md REVERT: 5c64366 update license banner in .ml files REVERT: c3cd260 Trying a better layout of hyperlinks on github REVERT: 2e15ff9 Trying a better layout of the .md on github REVERT: 8780445 Minor edition of the Announce. REVERT: 9adb947 Update ANNOUNCE-1.6.md REVERT: 672865b Merge branch 'master' of https://github.com/math-comp/math-comp REVERT: 732a8c3 Trailing whitespace removal REVERT: e22704b Ignore emacs checkpoints REVERT: 19ac062 Remove spurious injections REVERT: 03363b8 Explicit construction of finite fields REVERT: bafc4ee Some proof refactoring REVERT: 37f0673 Move finfield to field module REVERT: 058ec3b Add elementary abelian finite modules lemmas to abelian REVERT: 8318a82 Remove spurious injections REVERT: efc830f Add instances & lemmas for regular algebras REVERT: bd8cf1b Document limitation of fieldExtType cloning REVERT: 903a5e4 Correct improper CS declaration REVERT: a2b30aa Add finLmodType, finLalgType and finAlgType instances REVERT: 7737563 Removed spurious injection & clean up proof REVERT: 0b22709 Remove more redundant power type structures REVERT: 12ee0cf Correct join values to baseFingroupType REVERT: 70073eb Remove redundant structures for finite powers REVERT: 8a5defa Add missing export REVERT: e6076b2 fix coq-mathcomp-ssreflect opam package description REVERT: 0b02d10 better wording and package description in the ANNOUNCE for 1.6 REVERT: cfb8011 some work on installation instructions and annoucement message REVERT: 95354e0 Removing the only use of globTacticIn. REVERT: 7bf7dca add .mailmap to uniform names/email of committers REVERT: 1e388e3 fix compilation on trunk (thanks PMP) REVERT: c570d3d fix: autogen + abstract variables clash REVERT: 4d0f111 fix: elim/v handles eliminator from Derive Inversion (issue #2) REVERT: 55a5aaa Add commands to trace the matching algorithm REVERT: de9aafb fix: Hint View is not a Query REVERT: 2d032b5 Typos in comments. REVERT: 986f8d6 Tested the Qed of the alternate Xirredp_FAdjoin in Coq 8.4. REVERT: fb82de6 Typo. REVERT: c084774 Typos REVERT: da9bec4 fix INSTALL symlinks REVERT: c5fd978 Adding sections for definitions in change log REVERT: 490d8fa Update ChangeLog REVERT: ec504e2 ChangeLog: yake Yves' suggestion into account REVERT: 1058783 First stab at INSTALL REVERT: 6862e60 basic has disappeared REVERT: 98cfa7e Makefile to create a tar ball REVERT: 57b0dfb Changelog file created REVERT: eb65b7b Update .git* conf files to ignore/exclude cruft REVERT: 14c9a3a merge basic/ into ssreflect/ REVERT: 35124d2 Added support for highlighting 'isn't' in PG. REVERT: 254379d Added suport for highlighting gen(erally) have in PG. REVERT: 00643ca Small updates in the documentation of the customization of PG. REVERT: 6275cbd Restaured the config files (including doc) for PG in the ssreflect package. REVERT: b0e32f6 fix compilation on trunk REVERT: 39cc672 Fix compilation on 8.5 REVERT: ade7c12 Fix typo in README. REVERT: 14c940b Compare pattern heads (constants) up to "univs" REVERT: e9163a8 fix trunk compilation REVERT: d4deb12 Update README.md REVERT: 29a193a fix PF REVERT: 1e448cd add a missing From ... REVERT: a0d8980 Update README.md REVERT: 8e787d8 First stab at the README (displayed on github) REVERT: 627a555 fix Makefiles REVERT: 5ac5791 fix path of Makefile.coq-makefile REVERT: cd072f4 update copyright banner REVERT: 2e6d512 factor common Makefile stuff REVERT: ab80631 Add a From ... REVERT: 5558b68 next blind fix REVERT: 4a1a55b blind fix REVERT: f538fc0 blind patch by Enrico REVERT: ab387ba forgotten import REVERT: 32e4af5 remove duplicate fields REVERT: adc15de opam meta-data +url REVERT: 8047173 make the opam package meta data REVERT: 6d3dcee make opam meta-data REVERT: 663721c update opam meta-data REVERT: 7f7f8b1 keeping track of the changes for trunk (import from svn) REVERT: 152decf fix Makefile for trunk REVERT: d410a44 patch ssrcoqdep REVERT: 40021d4 update to preserve backward compatibility with v8.4 REVERT: 532de9b Updating files + reorganizing everything REVERT: f180c53 character for v8.5 REVERT: 2a89801 field for v8.5 REVERT: 999e5fd adapting solvable to 8.5 REVERT: c8b1f98 packaging odd_order REVERT: 634ee87 Using the From X Require Y for v8.4 REVERT: 1681e3b support for camlp4 REVERT: 0284fa8 Forward compatibility with "From X Require Y." REVERT: de1794e packaging for v8.5 REVERT: 858957a packaging for v8.5 REVERT: 737f79e makefiles that are version dependent REVERT: abe2354 Makefile, testing for v8.5 and uncommenting stuff REVERT: 9fa572c prepared discrete for compilation in v8.5 REVERT: 9859058 Merge pull request #1 from mattam82/master REVERT: 244e554 Fix Makefiles. REVERT: 22d788f fix gitignore REVERT: 9335bfa support both coq.8.5beta1 and coq.8.5.dev REVERT: 54d0e3b plugin that compiles with 8.5 REVERT: 4633066 The right way to ignore the plugin directory REVERT: e2530e7 Broken global Makefile REVERT: d226438 packaging all REVERT: 086f066 character packaged REVERT: 821071c packaging real_closed REVERT: f3671d3 change finfield from field to character REVERT: c7ddacd metadata for solvable and field REVERT: 0d2a1e7 packaging fingroup and algebra REVERT: 0c07923 remove undo files REVERT: 155e671 some work on ssreflect and discrete REVERT: fc84c27 Initial commit git-subtree-dir: htmldoc git-subtree-split: d7a61bb33774bc2e0a128e3127faea46e408ee12
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
testcase:
The text was updated successfully, but these errors were encountered: