diff options
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 6 | ||||
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 5 | ||||
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 3 | ||||
| -rw-r--r-- | interp/stdarg.ml | 4 | ||||
| -rw-r--r-- | interp/stdarg.mli | 3 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 1 | ||||
| -rw-r--r-- | plugins/cc/g_congruence.mlg | 4 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 3 |
8 files changed, 21 insertions, 8 deletions
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 66b6ffac89..a22f7ae9f3 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1087,10 +1087,10 @@ simple_tactic: [ | WITH "subst" OPT ( LIST1 var ) | DELETE "subst" | DELETE "congruence" -| DELETE "congruence" integer +| DELETE "congruence" natural | DELETE "congruence" "with" LIST1 constr -| REPLACE "congruence" integer "with" LIST1 constr -| WITH "congruence" OPT integer OPT ( "with" LIST1 constr ) +| REPLACE "congruence" natural "with" LIST1 constr +| WITH "congruence" OPT natural OPT ( "with" LIST1 constr ) | DELETE "show" "ltac" "profile" | REPLACE "show" "ltac" "profile" "cutoff" integer | WITH "show" "ltac" "profile" OPT [ "cutoff" integer | string ] diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 9614fc06fe..2ee8e4347e 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -689,6 +689,7 @@ command: [ | "Print" "Rings" (* setoid_ring plugin *) | "Add" "Field" ident ":" constr OPT field_mods (* setoid_ring plugin *) | "Print" "Fields" (* setoid_ring plugin *) +| "Number" "Notation" reference reference reference ":" ident numnotoption | "Numeral" "Notation" reference reference reference ":" ident numnotoption | "String" "Notation" reference reference reference ":" ident | "Ltac2" ltac2_entry (* Ltac2 plugin *) @@ -1435,9 +1436,9 @@ constr_as_binder_kind: [ simple_tactic: [ | "btauto" | "congruence" -| "congruence" integer +| "congruence" natural | "congruence" "with" LIST1 constr -| "congruence" integer "with" LIST1 constr +| "congruence" natural "with" LIST1 constr | "f_equal" | "firstorder" OPT tactic firstorder_using | "firstorder" OPT tactic "with" LIST1 preident diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index bbc4edf199..aae96fc966 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -896,6 +896,7 @@ command: [ | "Print" "Rings" (* setoid_ring plugin *) | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" ) (* setoid_ring plugin *) | "Print" "Fields" (* setoid_ring plugin *) +| "Number" "Notation" qualid qualid qualid ":" ident OPT numeral_modifier | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident ) | "Typeclasses" "Transparent" LIST0 qualid | "Typeclasses" "Opaque" LIST0 qualid @@ -1614,7 +1615,7 @@ simple_tactic: [ | "change_no_check" conversion OPT clause_dft_concl | "btauto" | "rtauto" -| "congruence" OPT integer OPT ( "with" LIST1 one_term ) +| "congruence" OPT natural OPT ( "with" LIST1 one_term ) | "f_equal" | "firstorder" OPT ltac_expr firstorder_rhs | "gintuition" OPT ltac_expr diff --git a/interp/stdarg.ml b/interp/stdarg.ml index d5f104b7f8..343f85be03 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -25,6 +25,9 @@ let wit_bool : bool uniform_genarg_type = let wit_int : int uniform_genarg_type = make0 "int" +let wit_nat : int uniform_genarg_type = + make0 "nat" + let wit_string : string uniform_genarg_type = make0 "string" @@ -59,6 +62,7 @@ let wit_clause_dft_concl = (** Aliases for compatibility *) let wit_integer = wit_int +let wit_natural = wit_nat let wit_preident = wit_pre_ident let wit_reference = wit_ref let wit_global = wit_ref diff --git a/interp/stdarg.mli b/interp/stdarg.mli index 89bdd78c70..3ae8b7d73f 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -23,6 +23,8 @@ val wit_unit : unit uniform_genarg_type val wit_bool : bool uniform_genarg_type +val wit_nat : int uniform_genarg_type + val wit_int : int uniform_genarg_type val wit_string : string uniform_genarg_type @@ -54,6 +56,7 @@ val wit_clause_dft_concl : (lident Locus.clause_expr, lident Locus.clause_expr, (** Aliases for compatibility *) +val wit_natural : int uniform_genarg_type val wit_integer : int uniform_genarg_type val wit_preident : string uniform_genarg_type val wit_reference : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index b9853029a0..0d74ad928c 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -500,6 +500,7 @@ let with_grammar_rule_protection f x = let () = let open Stdarg in + Grammar.register0 wit_nat (Prim.natural); Grammar.register0 wit_int (Prim.integer); Grammar.register0 wit_string (Prim.string); Grammar.register0 wit_pre_ident (Prim.preident); diff --git a/plugins/cc/g_congruence.mlg b/plugins/cc/g_congruence.mlg index 3920e3da75..2c91901477 100644 --- a/plugins/cc/g_congruence.mlg +++ b/plugins/cc/g_congruence.mlg @@ -22,9 +22,9 @@ DECLARE PLUGIN "cc_plugin" TACTIC EXTEND cc | [ "congruence" ] -> { congruence_tac 1000 [] } -| [ "congruence" integer(n) ] -> { congruence_tac n [] } +| [ "congruence" natural(n) ] -> { congruence_tac n [] } | [ "congruence" "with" ne_constr_list(l) ] -> { congruence_tac 1000 l } - |[ "congruence" integer(n) "with" ne_constr_list(l) ] -> +| [ "congruence" natural(n) "with" ne_constr_list(l) ] -> { congruence_tac n l } END diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 88480194c8..2258201c22 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -2028,6 +2028,9 @@ let () = declare_uniform wit_int let () = + declare_uniform wit_nat + +let () = declare_uniform wit_bool let () = |