diff options
| author | letouzey | 2012-08-11 13:33:26 +0000 |
|---|---|---|
| committer | letouzey | 2012-08-11 13:33:26 +0000 |
| commit | 5c825f263698433ed4e8db8ccd0c14394520535a (patch) | |
| tree | a9855a96d5e780166652b93376fea2483f9863c4 /tactics | |
| parent | c02c86626e36c908ec76854f8eda2d5278141d12 (diff) | |
fast bitwise operations (lor,land,lxor) on int31 and BigN
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15727 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/extraargs.ml4 | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 6d3a953526..7a47c51eef 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -383,7 +383,9 @@ PRINTED BY pr_r_int31_field | [ "int31" "compare" ] -> [ Retroknowledge.Int31Compare ] | [ "int31" "head0" ] -> [ Retroknowledge.Int31Head0 ] | [ "int31" "tail0" ] -> [ Retroknowledge.Int31Tail0 ] - +| [ "int31" "lor" ] -> [ Retroknowledge.Int31Lor ] +| [ "int31" "land" ] -> [ Retroknowledge.Int31Land ] +| [ "int31" "lxor" ] -> [ Retroknowledge.Int31Lxor ] END ARGUMENT EXTEND retroknowledge_field |