diff options
| author | bgregoir | 2007-06-20 09:43:36 +0000 |
|---|---|---|
| committer | bgregoir | 2007-06-20 09:43:36 +0000 |
| commit | f4586d1e8b1116340574d9660117f93e7a1e4e3b (patch) | |
| tree | 15b7dff4ed22b762446e4ae1f426e8f8aa2de52c /tactics | |
| parent | 4708506ca1b34e93835b163db102f6860c89190c (diff) | |
ajout de head0 et tail0 en natif
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9900 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/extraargs.ml4 | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 327bd24f79..c3377bca1f 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -282,9 +282,9 @@ let pr_r_int31_field _ _ _ i31f = let pr_retroknowledge_field _ _ _ f = match f with - | Retroknowledge.KEq -> str "equality" + (* | Retroknowledge.KEq -> str "equality" | Retroknowledge.KNat natf -> pr_r_nat_field () () () natf - | Retroknowledge.KN nf -> pr_r_n_field () () () nf + | Retroknowledge.KN nf -> pr_r_n_field () () () nf *) | Retroknowledge.KInt31 (group, i31f) -> (pr_r_int31_field () () () i31f) ++ str "in " ++ str group @@ -331,13 +331,16 @@ PRINTED BY pr_r_int31_field | [ "int31" "div" ] -> [ Retroknowledge.Int31Div ] | [ "int31" "addmuldiv" ] -> [ Retroknowledge.Int31AddMulDiv ] | [ "int31" "compare" ] -> [ Retroknowledge.Int31Compare ] +| [ "int31" "head0" ] -> [ Retroknowledge.Int31Head0 ] +| [ "int31" "tail0" ] -> [ Retroknowledge.Int31Tail0 ] + END ARGUMENT EXTEND retroknowledge_field TYPED AS r_field PRINTED BY pr_retroknowledge_field -| [ "equality" ] -> [ Retroknowledge.KEq ] +(*| [ "equality" ] -> [ Retroknowledge.KEq ] | [ retroknowledge_nat(n)] -> [ Retroknowledge.KNat n ] -| [ retroknowledge_binary_n (n)] -> [ Retroknowledge.KN n ] +| [ retroknowledge_binary_n (n)] -> [ Retroknowledge.KN n ]*) | [ retroknowledge_int31 (i) "in" string(g)] -> [ Retroknowledge.KInt31(g,i) ] -END
\ No newline at end of file +END |