aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/funind/glob_term_to_relation.ml2
-rw-r--r--plugins/ltac/g_tactic.mlg (renamed from plugins/ltac/g_tactic.ml4)452
-rw-r--r--plugins/ltac/tacentries.ml4
-rw-r--r--plugins/setoid_ring/g_newring.ml45
-rw-r--r--plugins/setoid_ring/newring.ml38
-rw-r--r--plugins/setoid_ring/newring.mli2
-rw-r--r--plugins/ssr/ssrparser.ml41
-rw-r--r--plugins/ssrmatching/g_ssrmatching.ml4101
-rw-r--r--plugins/ssrmatching/g_ssrmatching.mli17
-rw-r--r--plugins/ssrmatching/ssrmatching.ml (renamed from plugins/ssrmatching/ssrmatching.ml4)105
-rw-r--r--plugins/ssrmatching/ssrmatching.mli34
-rw-r--r--plugins/ssrmatching/ssrmatching_plugin.mlpack1
-rw-r--r--plugins/syntax/n_syntax.ml81
-rw-r--r--plugins/syntax/n_syntax_plugin.mlpack1
-rw-r--r--plugins/syntax/positive_syntax.ml101
-rw-r--r--plugins/syntax/positive_syntax_plugin.mlpack1
-rw-r--r--plugins/syntax/z_syntax.ml128
17 files changed, 597 insertions, 477 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 6b9b103122..5fc4293cbb 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1499,7 +1499,7 @@ let do_build_inductive
let _time2 = System.get_time () in
try
with_full_print
- (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false))
+ (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false ~uniform:ComInductive.NonUniformParameters))
Declarations.Finite
with
| UserError(s,msg) as e ->
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.mlg
index 31bc34a325..2e1ce814aa 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.mlg
@@ -8,6 +8,8 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+{
+
open Pp
open CErrors
open Util
@@ -215,486 +217,488 @@ let warn_deprecated_eqn_syntax =
open Pvernac.Vernac_
-GEXTEND Gram
+}
+
+GRAMMAR EXTEND Gram
GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
bindings red_expr int_or_var open_constr uconstr
simple_intropattern in_clause clause_dft_concl hypident destruction_arg;
int_or_var:
- [ [ n = integer -> ArgArg n
- | id = identref -> ArgVar id ] ]
+ [ [ n = integer -> { ArgArg n }
+ | id = identref -> { ArgVar id } ] ]
;
nat_or_var:
- [ [ n = natural -> ArgArg n
- | id = identref -> ArgVar id ] ]
+ [ [ n = natural -> { ArgArg n }
+ | id = identref -> { ArgVar id } ] ]
;
(* An identifier or a quotation meta-variable *)
id_or_meta:
- [ [ id = identref -> id ] ]
+ [ [ id = identref -> { id } ] ]
;
open_constr:
- [ [ c = constr -> c ] ]
+ [ [ c = constr -> { c } ] ]
;
uconstr:
- [ [ c = constr -> c ] ]
+ [ [ c = constr -> { c } ] ]
;
destruction_arg:
- [ [ n = natural -> (None,ElimOnAnonHyp n)
+ [ [ n = natural -> { (None,ElimOnAnonHyp n) }
| test_lpar_id_rpar; c = constr_with_bindings ->
- (Some false,destruction_arg_of_constr c)
- | c = constr_with_bindings_arg -> on_snd destruction_arg_of_constr c
+ { (Some false,destruction_arg_of_constr c) }
+ | c = constr_with_bindings_arg -> { on_snd destruction_arg_of_constr c }
] ]
;
constr_with_bindings_arg:
- [ [ ">"; c = constr_with_bindings -> (Some true,c)
- | c = constr_with_bindings -> (None,c) ] ]
+ [ [ ">"; c = constr_with_bindings -> { (Some true,c) }
+ | c = constr_with_bindings -> { (None,c) } ] ]
;
quantified_hypothesis:
- [ [ id = ident -> NamedHyp id
- | n = natural -> AnonHyp n ] ]
+ [ [ id = ident -> { NamedHyp id }
+ | n = natural -> { AnonHyp n } ] ]
;
conversion:
- [ [ c = constr -> (None, c)
- | c1 = constr; "with"; c2 = constr -> (Some (AllOccurrences,c1),c2)
+ [ [ c = constr -> { (None, c) }
+ | c1 = constr; "with"; c2 = constr -> { (Some (AllOccurrences,c1),c2) }
| c1 = constr; "at"; occs = occs_nums; "with"; c2 = constr ->
- (Some (occs,c1), c2) ] ]
+ { (Some (occs,c1), c2) } ] ]
;
occs_nums:
- [ [ nl = LIST1 nat_or_var -> OnlyOccurrences nl
+ [ [ nl = LIST1 nat_or_var -> { OnlyOccurrences nl }
| "-"; n = nat_or_var; nl = LIST0 int_or_var ->
(* have used int_or_var instead of nat_or_var for compatibility *)
- AllOccurrencesBut (List.map (map_int_or_var abs) (n::nl)) ] ]
+ { AllOccurrencesBut (List.map (map_int_or_var abs) (n::nl)) } ] ]
;
occs:
- [ [ "at"; occs = occs_nums -> occs | -> AllOccurrences ] ]
+ [ [ "at"; occs = occs_nums -> { occs } | -> { AllOccurrences } ] ]
;
pattern_occ:
- [ [ c = constr; nl = occs -> (nl,c) ] ]
+ [ [ c = constr; nl = occs -> { (nl,c) } ] ]
;
ref_or_pattern_occ:
(* If a string, it is interpreted as a ref
(anyway a Coq string does not reduce) *)
- [ [ c = smart_global; nl = occs -> nl,Inl c
- | c = constr; nl = occs -> nl,Inr c ] ]
+ [ [ c = smart_global; nl = occs -> { nl,Inl c }
+ | c = constr; nl = occs -> { nl,Inr c } ] ]
;
unfold_occ:
- [ [ c = smart_global; nl = occs -> (nl,c) ] ]
+ [ [ c = smart_global; nl = occs -> { (nl,c) } ] ]
;
intropatterns:
- [ [ l = LIST0 nonsimple_intropattern -> l ]]
+ [ [ l = LIST0 nonsimple_intropattern -> { l } ] ]
;
ne_intropatterns:
- [ [ l = LIST1 nonsimple_intropattern -> l ]]
+ [ [ l = LIST1 nonsimple_intropattern -> { l } ] ]
;
or_and_intropattern:
- [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> IntroOrPattern tc
- | "()" -> IntroAndPattern []
- | "("; si = simple_intropattern; ")" -> IntroAndPattern [si]
+ [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> { IntroOrPattern tc }
+ | "()" -> { IntroAndPattern [] }
+ | "("; si = simple_intropattern; ")" -> { IntroAndPattern [si] }
| "("; si = simple_intropattern; ",";
tc = LIST1 simple_intropattern SEP "," ; ")" ->
- IntroAndPattern (si::tc)
+ { IntroAndPattern (si::tc) }
| "("; si = simple_intropattern; "&";
tc = LIST1 simple_intropattern SEP "&" ; ")" ->
(* (A & B & C) is translated into (A,(B,C)) *)
- let rec pairify = function
+ { let rec pairify = function
| ([]|[_]|[_;_]) as l -> l
| t::q -> [t; CAst.make ?loc:(loc_of_ne_list q) (IntroAction (IntroOrAndPattern (IntroAndPattern (pairify q))))]
- in IntroAndPattern (pairify (si::tc)) ] ]
+ in IntroAndPattern (pairify (si::tc)) } ] ]
;
equality_intropattern:
- [ [ "->" -> IntroRewrite true
- | "<-" -> IntroRewrite false
- | "[="; tc = intropatterns; "]" -> IntroInjection tc ] ]
+ [ [ "->" -> { IntroRewrite true }
+ | "<-" -> { IntroRewrite false }
+ | "[="; tc = intropatterns; "]" -> { IntroInjection tc } ] ]
;
naming_intropattern:
- [ [ prefix = pattern_ident -> IntroFresh prefix
- | "?" -> IntroAnonymous
- | id = ident -> IntroIdentifier id ] ]
+ [ [ prefix = pattern_ident -> { IntroFresh prefix }
+ | "?" -> { IntroAnonymous }
+ | id = ident -> { IntroIdentifier id } ] ]
;
nonsimple_intropattern:
- [ [ l = simple_intropattern -> l
- | "*" -> CAst.make ~loc:!@loc @@ IntroForthcoming true
- | "**" -> CAst.make ~loc:!@loc @@ IntroForthcoming false ]]
+ [ [ l = simple_intropattern -> { l }
+ | "*" -> { CAst.make ~loc @@ IntroForthcoming true }
+ | "**" -> { CAst.make ~loc @@ IntroForthcoming false } ] ]
;
simple_intropattern:
[ [ pat = simple_intropattern_closed;
- l = LIST0 ["%"; c = operconstr LEVEL "0" -> c] ->
- let {CAst.loc=loc0;v=pat} = pat in
+ l = LIST0 ["%"; c = operconstr LEVEL "0" -> { c } ] ->
+ { let {CAst.loc=loc0;v=pat} = pat in
let f c pat =
let loc1 = Constrexpr_ops.constr_loc c in
let loc = Loc.merge_opt loc0 loc1 in
IntroAction (IntroApplyOn (CAst.(make ?loc:loc1 c),CAst.(make ?loc pat))) in
- CAst.make ~loc:!@loc @@ List.fold_right f l pat ] ]
+ CAst.make ~loc @@ List.fold_right f l pat } ] ]
;
simple_intropattern_closed:
- [ [ pat = or_and_intropattern -> CAst.make ~loc:!@loc @@ IntroAction (IntroOrAndPattern pat)
- | pat = equality_intropattern -> CAst.make ~loc:!@loc @@ IntroAction pat
- | "_" -> CAst.make ~loc:!@loc @@ IntroAction IntroWildcard
- | pat = naming_intropattern -> CAst.make ~loc:!@loc @@ IntroNaming pat ] ]
+ [ [ pat = or_and_intropattern -> { CAst.make ~loc @@ IntroAction (IntroOrAndPattern pat) }
+ | pat = equality_intropattern -> { CAst.make ~loc @@ IntroAction pat }
+ | "_" -> { CAst.make ~loc @@ IntroAction IntroWildcard }
+ | pat = naming_intropattern -> { CAst.make ~loc @@ IntroNaming pat } ] ]
;
simple_binding:
- [ [ "("; id = ident; ":="; c = lconstr; ")" -> CAst.make ~loc:!@loc (NamedHyp id, c)
- | "("; n = natural; ":="; c = lconstr; ")" -> CAst.make ~loc:!@loc (AnonHyp n, c) ] ]
+ [ [ "("; id = ident; ":="; c = lconstr; ")" -> { CAst.make ~loc (NamedHyp id, c) }
+ | "("; n = natural; ":="; c = lconstr; ")" -> { CAst.make ~loc (AnonHyp n, c) } ] ]
;
bindings:
[ [ test_lpar_idnum_coloneq; bl = LIST1 simple_binding ->
- ExplicitBindings bl
- | bl = LIST1 constr -> ImplicitBindings bl ] ]
+ { ExplicitBindings bl }
+ | bl = LIST1 constr -> { ImplicitBindings bl } ] ]
;
constr_with_bindings:
- [ [ c = constr; l = with_bindings -> (c, l) ] ]
+ [ [ c = constr; l = with_bindings -> { (c, l) } ] ]
;
with_bindings:
- [ [ "with"; bl = bindings -> bl | -> NoBindings ] ]
+ [ [ "with"; bl = bindings -> { bl } | -> { NoBindings } ] ]
;
red_flags:
- [ [ IDENT "beta" -> [FBeta]
- | IDENT "iota" -> [FMatch;FFix;FCofix]
- | IDENT "match" -> [FMatch]
- | IDENT "fix" -> [FFix]
- | IDENT "cofix" -> [FCofix]
- | IDENT "zeta" -> [FZeta]
- | IDENT "delta"; d = delta_flag -> [d]
+ [ [ IDENT "beta" -> { [FBeta] }
+ | IDENT "iota" -> { [FMatch;FFix;FCofix] }
+ | IDENT "match" -> { [FMatch] }
+ | IDENT "fix" -> { [FFix] }
+ | IDENT "cofix" -> { [FCofix] }
+ | IDENT "zeta" -> { [FZeta] }
+ | IDENT "delta"; d = delta_flag -> { [d] }
] ]
;
delta_flag:
- [ [ "-"; "["; idl = LIST1 smart_global; "]" -> FDeltaBut idl
- | "["; idl = LIST1 smart_global; "]" -> FConst idl
- | -> FDeltaBut []
+ [ [ "-"; "["; idl = LIST1 smart_global; "]" -> { FDeltaBut idl }
+ | "["; idl = LIST1 smart_global; "]" -> { FConst idl }
+ | -> { FDeltaBut [] }
] ]
;
strategy_flag:
- [ [ s = LIST1 red_flags -> Redops.make_red_flag (List.flatten s)
- | d = delta_flag -> all_with d
+ [ [ s = LIST1 red_flags -> { Redops.make_red_flag (List.flatten s) }
+ | d = delta_flag -> { all_with d }
] ]
;
red_expr:
- [ [ IDENT "red" -> Red false
- | IDENT "hnf" -> Hnf
- | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ -> Simpl (all_with d,po)
- | IDENT "cbv"; s = strategy_flag -> Cbv s
- | IDENT "cbn"; s = strategy_flag -> Cbn s
- | IDENT "lazy"; s = strategy_flag -> Lazy s
- | IDENT "compute"; delta = delta_flag -> Cbv (all_with delta)
- | IDENT "vm_compute"; po = OPT ref_or_pattern_occ -> CbvVm po
- | IDENT "native_compute"; po = OPT ref_or_pattern_occ -> CbvNative po
- | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul
- | IDENT "fold"; cl = LIST1 constr -> Fold cl
- | IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> Pattern pl
- | s = IDENT -> ExtraRedExpr s ] ]
+ [ [ IDENT "red" -> { Red false }
+ | IDENT "hnf" -> { Hnf }
+ | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ -> { Simpl (all_with d,po) }
+ | IDENT "cbv"; s = strategy_flag -> { Cbv s }
+ | IDENT "cbn"; s = strategy_flag -> { Cbn s }
+ | IDENT "lazy"; s = strategy_flag -> { Lazy s }
+ | IDENT "compute"; delta = delta_flag -> { Cbv (all_with delta) }
+ | IDENT "vm_compute"; po = OPT ref_or_pattern_occ -> { CbvVm po }
+ | IDENT "native_compute"; po = OPT ref_or_pattern_occ -> { CbvNative po }
+ | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> { Unfold ul }
+ | IDENT "fold"; cl = LIST1 constr -> { Fold cl }
+ | IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> { Pattern pl }
+ | s = IDENT -> { ExtraRedExpr s } ] ]
;
hypident:
[ [ id = id_or_meta ->
- let id : lident = id in
- id,InHyp
+ { let id : lident = id in
+ id,InHyp }
| "("; IDENT "type"; IDENT "of"; id = id_or_meta; ")" ->
- let id : lident = id in
- id,InHypTypeOnly
+ { let id : lident = id in
+ id,InHypTypeOnly }
| "("; IDENT "value"; IDENT "of"; id = id_or_meta; ")" ->
- let id : lident = id in
- id,InHypValueOnly
+ { let id : lident = id in
+ id,InHypValueOnly }
] ]
;
hypident_occ:
- [ [ (id,l)=hypident; occs=occs ->
+ [ [ h=hypident; occs=occs ->
+ { let (id,l) = h in
let id : lident = id in
- ((occs,id),l) ] ]
+ ((occs,id),l) } ] ]
;
in_clause:
[ [ "*"; occs=occs ->
- {onhyps=None; concl_occs=occs}
+ { {onhyps=None; concl_occs=occs} }
| "*"; "|-"; occs=concl_occ ->
- {onhyps=None; concl_occs=occs}
+ { {onhyps=None; concl_occs=occs} }
| hl=LIST0 hypident_occ SEP","; "|-"; occs=concl_occ ->
- {onhyps=Some hl; concl_occs=occs}
+ { {onhyps=Some hl; concl_occs=occs} }
| hl=LIST0 hypident_occ SEP"," ->
- {onhyps=Some hl; concl_occs=NoOccurrences} ] ]
+ { {onhyps=Some hl; concl_occs=NoOccurrences} } ] ]
;
clause_dft_concl:
- [ [ "in"; cl = in_clause -> cl
- | occs=occs -> {onhyps=Some[]; concl_occs=occs}
- | -> all_concl_occs_clause ] ]
+ [ [ "in"; cl = in_clause -> { cl }
+ | occs=occs -> { {onhyps=Some[]; concl_occs=occs} }
+ | -> { all_concl_occs_clause } ] ]
;
clause_dft_all:
- [ [ "in"; cl = in_clause -> cl
- | -> {onhyps=None; concl_occs=AllOccurrences} ] ]
+ [ [ "in"; cl = in_clause -> { cl }
+ | -> { {onhyps=None; concl_occs=AllOccurrences} } ] ]
;
opt_clause:
- [ [ "in"; cl = in_clause -> Some cl
- | "at"; occs = occs_nums -> Some {onhyps=Some[]; concl_occs=occs}
- | -> None ] ]
+ [ [ "in"; cl = in_clause -> { Some cl }
+ | "at"; occs = occs_nums -> { Some {onhyps=Some[]; concl_occs=occs} }
+ | -> { None } ] ]
;
concl_occ:
- [ [ "*"; occs = occs -> occs
- | -> NoOccurrences ] ]
+ [ [ "*"; occs = occs -> { occs }
+ | -> { NoOccurrences } ] ]
;
in_hyp_list:
- [ [ "in"; idl = LIST1 id_or_meta -> idl
- | -> [] ] ]
+ [ [ "in"; idl = LIST1 id_or_meta -> { idl }
+ | -> { [] } ] ]
;
in_hyp_as:
- [ [ "in"; id = id_or_meta; ipat = as_ipat -> Some (id,ipat)
- | -> None ] ]
+ [ [ "in"; id = id_or_meta; ipat = as_ipat -> { Some (id,ipat) }
+ | -> { None } ] ]
;
orient:
- [ [ "->" -> true
- | "<-" -> false
- | -> true ]]
+ [ [ "->" -> { true }
+ | "<-" -> { false }
+ | -> { true } ] ]
;
simple_binder:
- [ [ na=name -> ([na],Default Explicit, CAst.make ~loc:!@loc @@
- CHole (Some (Evar_kinds.BinderType na.CAst.v), IntroAnonymous, None))
- | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> (nal,Default Explicit,c)
+ [ [ na=name -> { ([na],Default Explicit, CAst.make ~loc @@
+ CHole (Some (Evar_kinds.BinderType na.CAst.v), IntroAnonymous, None)) }
+ | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> { (nal,Default Explicit,c) }
] ]
;
fixdecl:
[ [ "("; id = ident; bl=LIST0 simple_binder; ann=fixannot;
- ":"; ty=lconstr; ")" -> (!@loc, id, bl, ann, ty) ] ]
+ ":"; ty=lconstr; ")" -> { (loc, id, bl, ann, ty) } ] ]
;
fixannot:
- [ [ "{"; IDENT "struct"; id=name; "}" -> Some id
- | -> None ] ]
+ [ [ "{"; IDENT "struct"; id=name; "}" -> { Some id }
+ | -> { None } ] ]
;
cofixdecl:
[ [ "("; id = ident; bl=LIST0 simple_binder; ":"; ty=lconstr; ")" ->
- (!@loc, id, bl, None, ty) ] ]
+ { (loc, id, bl, None, ty) } ] ]
;
bindings_with_parameters:
[ [ check_for_coloneq; "("; id = ident; bl = LIST0 simple_binder;
- ":="; c = lconstr; ")" -> (id, mkCLambdaN_simple bl c) ] ]
+ ":="; c = lconstr; ")" -> { (id, mkCLambdaN_simple bl c) } ] ]
;
eliminator:
- [ [ "using"; el = constr_with_bindings -> el ] ]
+ [ [ "using"; el = constr_with_bindings -> { el } ] ]
;
as_ipat:
- [ [ "as"; ipat = simple_intropattern -> Some ipat
- | -> None ] ]
+ [ [ "as"; ipat = simple_intropattern -> { Some ipat }
+ | -> { None } ] ]
;
or_and_intropattern_loc:
- [ [ ipat = or_and_intropattern -> ArgArg (CAst.make ~loc:!@loc ipat)
- | locid = identref -> ArgVar locid ] ]
+ [ [ ipat = or_and_intropattern -> { ArgArg (CAst.make ~loc ipat) }
+ | locid = identref -> { ArgVar locid } ] ]
;
as_or_and_ipat:
- [ [ "as"; ipat = or_and_intropattern_loc -> Some ipat
- | -> None ] ]
+ [ [ "as"; ipat = or_and_intropattern_loc -> { Some ipat }
+ | -> { None } ] ]
;
eqn_ipat:
- [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some (CAst.make ~loc:!@loc pat)
+ [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> { Some (CAst.make ~loc pat) }
| IDENT "_eqn"; ":"; pat = naming_intropattern ->
- let loc = !@loc in
- warn_deprecated_eqn_syntax ~loc "H"; Some (CAst.make ~loc pat)
+ { warn_deprecated_eqn_syntax ~loc "H"; Some (CAst.make ~loc pat) }
| IDENT "_eqn" ->
- let loc = !@loc in
- warn_deprecated_eqn_syntax ~loc "?"; Some (CAst.make ~loc IntroAnonymous)
- | -> None ] ]
+ { warn_deprecated_eqn_syntax ~loc "?"; Some (CAst.make ~loc IntroAnonymous) }
+ | -> { None } ] ]
;
as_name:
- [ [ "as"; id = ident ->Names.Name.Name id | -> Names.Name.Anonymous ] ]
+ [ [ "as"; id = ident -> { Names.Name.Name id } | -> { Names.Name.Anonymous } ] ]
;
by_tactic:
- [ [ "by"; tac = tactic_expr LEVEL "3" -> Some tac
- | -> None ] ]
+ [ [ "by"; tac = tactic_expr LEVEL "3" -> { Some tac }
+ | -> { None } ] ]
;
rewriter :
- [ [ "!"; c = constr_with_bindings_arg -> (Equality.RepeatPlus,c)
- | ["?"| LEFTQMARK]; c = constr_with_bindings_arg -> (Equality.RepeatStar,c)
- | n = natural; "!"; c = constr_with_bindings_arg -> (Equality.Precisely n,c)
- | n = natural; ["?" | LEFTQMARK]; c = constr_with_bindings_arg -> (Equality.UpTo n,c)
- | n = natural; c = constr_with_bindings_arg -> (Equality.Precisely n,c)
- | c = constr_with_bindings_arg -> (Equality.Precisely 1, c)
+ [ [ "!"; c = constr_with_bindings_arg -> { (Equality.RepeatPlus,c) }
+ | ["?" -> { () } | LEFTQMARK -> { () } ]; c = constr_with_bindings_arg -> { (Equality.RepeatStar,c) }
+ | n = natural; "!"; c = constr_with_bindings_arg -> { (Equality.Precisely n,c) }
+ | n = natural; ["?" -> { () } | LEFTQMARK -> { () } ]; c = constr_with_bindings_arg -> { (Equality.UpTo n,c) }
+ | n = natural; c = constr_with_bindings_arg -> { (Equality.Precisely n,c) }
+ | c = constr_with_bindings_arg -> { (Equality.Precisely 1, c) }
] ]
;
oriented_rewriter :
- [ [ b = orient; p = rewriter -> let (m,c) = p in (b,m,c) ] ]
+ [ [ b = orient; p = rewriter -> { let (m,c) = p in (b,m,c) } ] ]
;
induction_clause:
[ [ c = destruction_arg; pat = as_or_and_ipat; eq = eqn_ipat;
- cl = opt_clause -> (c,(eq,pat),cl) ] ]
+ cl = opt_clause -> { (c,(eq,pat),cl) } ] ]
;
induction_clause_list:
[ [ ic = LIST1 induction_clause SEP ","; el = OPT eliminator;
cl_tolerance = opt_clause ->
(* Condition for accepting "in" at the end by compatibility *)
- match ic,el,cl_tolerance with
+ { match ic,el,cl_tolerance with
| [c,pat,None],Some _,Some _ -> ([c,pat,cl_tolerance],el)
| _,_,Some _ -> err ()
- | _,_,None -> (ic,el) ]]
+ | _,_,None -> (ic,el) } ] ]
;
simple_tactic:
[ [
(* Basic tactics *)
IDENT "intros"; pl = ne_intropatterns ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (false,pl))
+ { TacAtom (Loc.tag ~loc @@ TacIntroPattern (false,pl)) }
| IDENT "intros" ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (false,[CAst.make ~loc:!@loc @@IntroForthcoming false]))
+ { TacAtom (Loc.tag ~loc @@ TacIntroPattern (false,[CAst.make ~loc @@IntroForthcoming false])) }
| IDENT "eintros"; pl = ne_intropatterns ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (true,pl))
+ { TacAtom (Loc.tag ~loc @@ TacIntroPattern (true,pl)) }
| IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ",";
- inhyp = in_hyp_as -> TacAtom (Loc.tag ~loc:!@loc @@ TacApply (true,false,cl,inhyp))
+ inhyp = in_hyp_as -> { TacAtom (Loc.tag ~loc @@ TacApply (true,false,cl,inhyp)) }
| IDENT "eapply"; cl = LIST1 constr_with_bindings_arg SEP ",";
- inhyp = in_hyp_as -> TacAtom (Loc.tag ~loc:!@loc @@ TacApply (true,true,cl,inhyp))
+ inhyp = in_hyp_as -> { TacAtom (Loc.tag ~loc @@ TacApply (true,true,cl,inhyp)) }
| IDENT "simple"; IDENT "apply";
cl = LIST1 constr_with_bindings_arg SEP ",";
- inhyp = in_hyp_as -> TacAtom (Loc.tag ~loc:!@loc @@ TacApply (false,false,cl,inhyp))
+ inhyp = in_hyp_as -> { TacAtom (Loc.tag ~loc @@ TacApply (false,false,cl,inhyp)) }
| IDENT "simple"; IDENT "eapply";
cl = LIST1 constr_with_bindings_arg SEP",";
- inhyp = in_hyp_as -> TacAtom (Loc.tag ~loc:!@loc @@ TacApply (false,true,cl,inhyp))
+ inhyp = in_hyp_as -> { TacAtom (Loc.tag ~loc @@ TacApply (false,true,cl,inhyp)) }
| IDENT "elim"; cl = constr_with_bindings_arg; el = OPT eliminator ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacElim (false,cl,el))
+ { TacAtom (Loc.tag ~loc @@ TacElim (false,cl,el)) }
| IDENT "eelim"; cl = constr_with_bindings_arg; el = OPT eliminator ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacElim (true,cl,el))
- | IDENT "case"; icl = induction_clause_list -> TacAtom (Loc.tag ~loc:!@loc @@ mkTacCase false icl)
- | IDENT "ecase"; icl = induction_clause_list -> TacAtom (Loc.tag ~loc:!@loc @@ mkTacCase true icl)
+ { TacAtom (Loc.tag ~loc @@ TacElim (true,cl,el)) }
+ | IDENT "case"; icl = induction_clause_list -> { TacAtom (Loc.tag ~loc @@ mkTacCase false icl) }
+ | IDENT "ecase"; icl = induction_clause_list -> { TacAtom (Loc.tag ~loc @@ mkTacCase true icl) }
| "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacMutualFix (id,n,List.map mk_fix_tac fd))
+ { TacAtom (Loc.tag ~loc @@ TacMutualFix (id,n,List.map mk_fix_tac fd)) }
| "cofix"; id = ident; "with"; fd = LIST1 cofixdecl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacMutualCofix (id,List.map mk_cofix_tac fd))
+ { TacAtom (Loc.tag ~loc @@ TacMutualCofix (id,List.map mk_cofix_tac fd)) }
- | IDENT "pose"; (id,b) = bindings_with_parameters ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,Names.Name.Name id,b,Locusops.nowhere,true,None))
+ | IDENT "pose"; bl = bindings_with_parameters ->
+ { let (id,b) = bl in TacAtom (Loc.tag ~loc @@ TacLetTac (false,Names.Name.Name id,b,Locusops.nowhere,true,None)) }
| IDENT "pose"; b = constr; na = as_name ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,b,Locusops.nowhere,true,None))
- | IDENT "epose"; (id,b) = bindings_with_parameters ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,Names.Name id,b,Locusops.nowhere,true,None))
+ { TacAtom (Loc.tag ~loc @@ TacLetTac (false,na,b,Locusops.nowhere,true,None)) }
+ | IDENT "epose"; bl = bindings_with_parameters ->
+ { let (id,b) = bl in TacAtom (Loc.tag ~loc @@ TacLetTac (true,Names.Name id,b,Locusops.nowhere,true,None)) }
| IDENT "epose"; b = constr; na = as_name ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,b,Locusops.nowhere,true,None))
- | IDENT "set"; (id,c) = bindings_with_parameters; p = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,Names.Name.Name id,c,p,true,None))
+ { TacAtom (Loc.tag ~loc @@ TacLetTac (true,na,b,Locusops.nowhere,true,None)) }
+ | IDENT "set"; bl = bindings_with_parameters; p = clause_dft_concl ->
+ { let (id,c) = bl in TacAtom (Loc.tag ~loc @@ TacLetTac (false,Names.Name.Name id,c,p,true,None)) }
| IDENT "set"; c = constr; na = as_name; p = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,c,p,true,None))
- | IDENT "eset"; (id,c) = bindings_with_parameters; p = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,Names.Name id,c,p,true,None))
+ { TacAtom (Loc.tag ~loc @@ TacLetTac (false,na,c,p,true,None)) }
+ | IDENT "eset"; bl = bindings_with_parameters; p = clause_dft_concl ->
+ { let (id,c) = bl in TacAtom (Loc.tag ~loc @@ TacLetTac (true,Names.Name id,c,p,true,None)) }
| IDENT "eset"; c = constr; na = as_name; p = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,c,p,true,None))
+ { TacAtom (Loc.tag ~loc @@ TacLetTac (true,na,c,p,true,None)) }
| IDENT "remember"; c = constr; na = as_name; e = eqn_ipat;
p = clause_dft_all ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,c,p,false,e))
+ { TacAtom (Loc.tag ~loc @@ TacLetTac (false,na,c,p,false,e)) }
| IDENT "eremember"; c = constr; na = as_name; e = eqn_ipat;
p = clause_dft_all ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,c,p,false,e))
+ { TacAtom (Loc.tag ~loc @@ TacLetTac (true,na,c,p,false,e)) }
(* Alternative syntax for "pose proof c as id" *)
| IDENT "assert"; test_lpar_id_coloneq; "("; lid = identref; ":=";
c = lconstr; ")" ->
- let { CAst.loc = loc; v = id } = lid in
- TacAtom (Loc.tag ?loc @@ TacAssert (false,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c))
+ { let { CAst.loc = loc; v = id } = lid in
+ TacAtom (Loc.tag ?loc @@ TacAssert (false,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
| IDENT "eassert"; test_lpar_id_coloneq; "("; lid = identref; ":=";
c = lconstr; ")" ->
- let { CAst.loc = loc; v = id } = lid in
- TacAtom (Loc.tag ?loc @@ TacAssert (true,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c))
+ { let { CAst.loc = loc; v = id } = lid in
+ TacAtom (Loc.tag ?loc @@ TacAssert (true,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
(* Alternative syntax for "assert c as id by tac" *)
| IDENT "assert"; test_lpar_id_colon; "("; lid = identref; ":";
c = lconstr; ")"; tac=by_tactic ->
- let { CAst.loc = loc; v = id } = lid in
- TacAtom (Loc.tag ?loc @@ TacAssert (false,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c))
+ { let { CAst.loc = loc; v = id } = lid in
+ TacAtom (Loc.tag ?loc @@ TacAssert (false,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
| IDENT "eassert"; test_lpar_id_colon; "("; lid = identref; ":";
c = lconstr; ")"; tac=by_tactic ->
- let { CAst.loc = loc; v = id } = lid in
- TacAtom (Loc.tag ?loc @@ TacAssert (true,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c))
+ { let { CAst.loc = loc; v = id } = lid in
+ TacAtom (Loc.tag ?loc @@ TacAssert (true,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
(* Alternative syntax for "enough c as id by tac" *)
| IDENT "enough"; test_lpar_id_colon; "("; lid = identref; ":";
c = lconstr; ")"; tac=by_tactic ->
- let { CAst.loc = loc; v = id } = lid in
- TacAtom (Loc.tag ?loc @@ TacAssert (false,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c))
+ { let { CAst.loc = loc; v = id } = lid in
+ TacAtom (Loc.tag ?loc @@ TacAssert (false,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
| IDENT "eenough"; test_lpar_id_colon; "("; lid = identref; ":";
c = lconstr; ")"; tac=by_tactic ->
- let { CAst.loc = loc; v = id } = lid in
- TacAtom (Loc.tag ?loc @@ TacAssert (true,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c))
+ { let { CAst.loc = loc; v = id } = lid in
+ TacAtom (Loc.tag ?loc @@ TacAssert (true,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
| IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,Some tac,ipat,c))
+ { TacAtom (Loc.tag ~loc @@ TacAssert (false,true,Some tac,ipat,c)) }
| IDENT "eassert"; c = constr; ipat = as_ipat; tac = by_tactic ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,Some tac,ipat,c))
+ { TacAtom (Loc.tag ~loc @@ TacAssert (true,true,Some tac,ipat,c)) }
| IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,None,ipat,c))
+ { TacAtom (Loc.tag ~loc @@ TacAssert (false,true,None,ipat,c)) }
| IDENT "epose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,None,ipat,c))
+ { TacAtom (Loc.tag ~loc @@ TacAssert (true,true,None,ipat,c)) }
| IDENT "enough"; c = constr; ipat = as_ipat; tac = by_tactic ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,false,Some tac,ipat,c))
+ { TacAtom (Loc.tag ~loc @@ TacAssert (false,false,Some tac,ipat,c)) }
| IDENT "eenough"; c = constr; ipat = as_ipat; tac = by_tactic ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,false,Some tac,ipat,c))
+ { TacAtom (Loc.tag ~loc @@ TacAssert (true,false,Some tac,ipat,c)) }
| IDENT "generalize"; c = constr ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize [((AllOccurrences,c),Names.Name.Anonymous)])
+ { TacAtom (Loc.tag ~loc @@ TacGeneralize [((AllOccurrences,c),Names.Name.Anonymous)]) }
| IDENT "generalize"; c = constr; l = LIST1 constr ->
- let gen_everywhere c = ((AllOccurrences,c),Names.Name.Anonymous) in
- TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize (List.map gen_everywhere (c::l)))
+ { let gen_everywhere c = ((AllOccurrences,c),Names.Name.Anonymous) in
+ TacAtom (Loc.tag ~loc @@ TacGeneralize (List.map gen_everywhere (c::l))) }
| IDENT "generalize"; c = constr; lookup_at_as_comma; nl = occs;
na = as_name;
- l = LIST0 [","; c = pattern_occ; na = as_name -> (c,na)] ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize (((nl,c),na)::l))
+ l = LIST0 [","; c = pattern_occ; na = as_name -> { (c,na) } ] ->
+ { TacAtom (Loc.tag ~loc @@ TacGeneralize (((nl,c),na)::l)) }
(* Derived basic tactics *)
| IDENT "induction"; ic = induction_clause_list ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacInductionDestruct (true,false,ic))
+ { TacAtom (Loc.tag ~loc @@ TacInductionDestruct (true,false,ic)) }
| IDENT "einduction"; ic = induction_clause_list ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacInductionDestruct(true,true,ic))
+ { TacAtom (Loc.tag ~loc @@ TacInductionDestruct(true,true,ic)) }
| IDENT "destruct"; icl = induction_clause_list ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacInductionDestruct(false,false,icl))
+ { TacAtom (Loc.tag ~loc @@ TacInductionDestruct(false,false,icl)) }
| IDENT "edestruct"; icl = induction_clause_list ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacInductionDestruct(false,true,icl))
+ { TacAtom (Loc.tag ~loc @@ TacInductionDestruct(false,true,icl)) }
(* Equality and inversion *)
| IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ",";
- cl = clause_dft_concl; t=by_tactic -> TacAtom (Loc.tag ~loc:!@loc @@ TacRewrite (false,l,cl,t))
+ cl = clause_dft_concl; t=by_tactic -> { TacAtom (Loc.tag ~loc @@ TacRewrite (false,l,cl,t)) }
| IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ",";
- cl = clause_dft_concl; t=by_tactic -> TacAtom (Loc.tag ~loc:!@loc @@ TacRewrite (true,l,cl,t))
+ cl = clause_dft_concl; t=by_tactic -> { TacAtom (Loc.tag ~loc @@ TacRewrite (true,l,cl,t)) }
| IDENT "dependent"; k =
- [ IDENT "simple"; IDENT "inversion" -> SimpleInversion
- | IDENT "inversion" -> FullInversion
- | IDENT "inversion_clear" -> FullInversionClear ];
+ [ IDENT "simple"; IDENT "inversion" -> { SimpleInversion }
+ | IDENT "inversion" -> { FullInversion }
+ | IDENT "inversion_clear" -> { FullInversionClear } ];
hyp = quantified_hypothesis;
- ids = as_or_and_ipat; co = OPT ["with"; c = constr -> c] ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (DepInversion (k,co,ids),hyp))
+ ids = as_or_and_ipat; co = OPT ["with"; c = constr -> { c } ] ->
+ { TacAtom (Loc.tag ~loc @@ TacInversion (DepInversion (k,co,ids),hyp)) }
| IDENT "simple"; IDENT "inversion";
hyp = quantified_hypothesis; ids = as_or_and_ipat;
cl = in_hyp_list ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp))
+ { TacAtom (Loc.tag ~loc @@ TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp)) }
| IDENT "inversion";
hyp = quantified_hypothesis; ids = as_or_and_ipat;
cl = in_hyp_list ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (NonDepInversion (FullInversion, cl, ids), hyp))
+ { TacAtom (Loc.tag ~loc @@ TacInversion (NonDepInversion (FullInversion, cl, ids), hyp)) }
| IDENT "inversion_clear";
hyp = quantified_hypothesis; ids = as_or_and_ipat;
cl = in_hyp_list ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp))
+ { TacAtom (Loc.tag ~loc @@ TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp)) }
| IDENT "inversion"; hyp = quantified_hypothesis;
"using"; c = constr; cl = in_hyp_list ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (InversionUsing (c,cl), hyp))
+ { TacAtom (Loc.tag ~loc @@ TacInversion (InversionUsing (c,cl), hyp)) }
(* Conversion *)
| IDENT "red"; cl = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Red false, cl))
+ { TacAtom (Loc.tag ~loc @@ TacReduce (Red false, cl)) }
| IDENT "hnf"; cl = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Hnf, cl))
+ { TacAtom (Loc.tag ~loc @@ TacReduce (Hnf, cl)) }
| IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Simpl (all_with d, po), cl))
+ { TacAtom (Loc.tag ~loc @@ TacReduce (Simpl (all_with d, po), cl)) }
| IDENT "cbv"; s = strategy_flag; cl = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Cbv s, cl))
+ { TacAtom (Loc.tag ~loc @@ TacReduce (Cbv s, cl)) }
| IDENT "cbn"; s = strategy_flag; cl = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Cbn s, cl))
+ { TacAtom (Loc.tag ~loc @@ TacReduce (Cbn s, cl)) }
| IDENT "lazy"; s = strategy_flag; cl = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Lazy s, cl))
+ { TacAtom (Loc.tag ~loc @@ TacReduce (Lazy s, cl)) }
| IDENT "compute"; delta = delta_flag; cl = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Cbv (all_with delta), cl))
+ { TacAtom (Loc.tag ~loc @@ TacReduce (Cbv (all_with delta), cl)) }
| IDENT "vm_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (CbvVm po, cl))
+ { TacAtom (Loc.tag ~loc @@ TacReduce (CbvVm po, cl)) }
| IDENT "native_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (CbvNative po, cl))
+ { TacAtom (Loc.tag ~loc @@ TacReduce (CbvNative po, cl)) }
| IDENT "unfold"; ul = LIST1 unfold_occ SEP ","; cl = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Unfold ul, cl))
+ { TacAtom (Loc.tag ~loc @@ TacReduce (Unfold ul, cl)) }
| IDENT "fold"; l = LIST1 constr; cl = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Fold l, cl))
+ { TacAtom (Loc.tag ~loc @@ TacReduce (Fold l, cl)) }
| IDENT "pattern"; pl = LIST1 pattern_occ SEP","; cl = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Pattern pl, cl))
+ { TacAtom (Loc.tag ~loc @@ TacReduce (Pattern pl, cl)) }
(* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
- | IDENT "change"; (oc,c) = conversion; cl = clause_dft_concl ->
- let p,cl = merge_occurrences (!@loc) cl oc in
- TacAtom (Loc.tag ~loc:!@loc @@ TacChange (p,c,cl))
+ | IDENT "change"; c = conversion; cl = clause_dft_concl ->
+ { let (oc, c) = c in
+ let p,cl = merge_occurrences loc cl oc in
+ TacAtom (Loc.tag ~loc @@ TacChange (p,c,cl)) }
] ]
;
-END;;
+END
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 98d4515367..876e6f3201 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -45,7 +45,7 @@ let coincide s pat off =
let atactic n =
if n = 5 then Aentry Pltac.binder_tactic
- else Aentryl (Pltac.tactic_expr, n)
+ else Aentryl (Pltac.tactic_expr, string_of_int n)
type entry_name = EntryName :
'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) Extend.symbol -> entry_name
@@ -398,7 +398,7 @@ let create_ltac_quotation name cast (e, l) =
let () = ltac_quotations := String.Set.add name !ltac_quotations in
let entry = match l with
| None -> Aentry e
- | Some l -> Aentryl (e, l)
+ | Some l -> Aentryl (e, string_of_int l)
in
(* let level = Some "1" in *)
let level = None in
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index e9ce306e86..4ea0b30bd7 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -29,11 +29,6 @@ TACTIC EXTEND protect_fv
[ protect_tac map ]
END
-TACTIC EXTEND closed_term
- [ "closed_term" constr(t) "[" ne_reference_list(l) "]" ] ->
- [ closed_term t l ]
-END
-
open Pptactic
open Ppconstr
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index e4d17f2504..8e0ca877a0 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -96,34 +96,36 @@ let protect_tac_in map id =
(****************************************************************************)
-let closed_term t l =
- let open Quote_plugin in
+let rec closed_under sigma cset t =
+ try
+ let (gr, _) = Termops.global_of_constr sigma t in
+ Refset_env.mem gr cset
+ with Not_found ->
+ match EConstr.kind sigma t with
+ | Cast(c,_,_) -> closed_under sigma cset c
+ | App(f,l) -> closed_under sigma cset f && Array.for_all (closed_under sigma cset) l
+ | _ -> false
+
+let closed_term args _ = match args with
+| [t; l] ->
+ let t = Option.get (Value.to_constr t) in
+ let l = List.map (fun c -> Value.cast (Genarg.topwit Stdarg.wit_ref) c) (Option.get (Value.to_list l)) in
Proofview.tclEVARMAP >>= fun sigma ->
- let l = List.map UnivGen.constr_of_global l in
- let cs = List.fold_right Quote.ConstrSet.add l Quote.ConstrSet.empty in
- if Quote.closed_under sigma cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt())
-
-(* TACTIC EXTEND echo
-| [ "echo" constr(t) ] ->
- [ Pp.msg (Termops.print_constr t); Tacinterp.eval_tactic (TacId []) ]
-END;;*)
+ let cs = List.fold_right Refset_env.add l Refset_env.empty in
+ if closed_under sigma cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt())
+| _ -> assert false
-(*
-let closed_term_ast l =
- TacFun([Some(Id.of_string"t")],
- TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term",
- [Genarg.in_gen Constrarg.wit_constr (mkVar(Id.of_string"t"));
- Genarg.in_gen (Genarg.wit_list Constrarg.wit_ref) l])))
-*)
-let closed_term_ast l =
+let closed_term_ast =
let tacname = {
mltac_plugin = "newring_plugin";
mltac_tactic = "closed_term";
} in
+ let () = Tacenv.register_ml_tactic tacname [|closed_term|] in
let tacname = {
mltac_name = tacname;
mltac_index = 0;
} in
+ fun l ->
let l = List.map (fun gr -> ArgArg(Loc.tag gr)) l in
TacFun([Name(Id.of_string"t")],
TacML(Loc.tag (tacname,
diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli
index 0e056a4722..fcd04a2e73 100644
--- a/plugins/setoid_ring/newring.mli
+++ b/plugins/setoid_ring/newring.mli
@@ -18,8 +18,6 @@ val protect_tac_in : string -> Id.t -> unit Proofview.tactic
val protect_tac : string -> unit Proofview.tactic
-val closed_term : EConstr.constr -> GlobRef.t list -> unit Proofview.tactic
-
val add_theory :
Id.t ->
constr_expr ->
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 347a1e4e26..6b183dab1c 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -962,6 +962,7 @@ END
(* the default simpl and unfold tactics would erase blindly. *)
open Ssrmatching_plugin.Ssrmatching
+open Ssrmatching_plugin.G_ssrmatching
let pr_wgen = function
| (clr, Some((id,k),None)) -> spc() ++ pr_clear mt clr ++ str k ++ pr_hoi id
diff --git a/plugins/ssrmatching/g_ssrmatching.ml4 b/plugins/ssrmatching/g_ssrmatching.ml4
new file mode 100644
index 0000000000..746c368aa9
--- /dev/null
+++ b/plugins/ssrmatching/g_ssrmatching.ml4
@@ -0,0 +1,101 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Ltac_plugin
+open Genarg
+open Pcoq
+open Pcoq.Constr
+open Ssrmatching
+open Ssrmatching.Internal
+
+(* Defining grammar rules with "xx" in it automatically declares keywords too,
+ * we thus save the lexer to restore it at the end of the file *)
+let frozen_lexer = CLexer.get_keyword_state () ;;
+
+DECLARE PLUGIN "ssrmatching_plugin"
+
+let pr_rpattern _ _ _ = pr_rpattern
+
+ARGUMENT EXTEND rpattern
+ TYPED AS rpatternty
+ PRINTED BY pr_rpattern
+ INTERPRETED BY interp_rpattern
+ GLOBALIZED BY glob_rpattern
+ SUBSTITUTED BY subst_rpattern
+ | [ lconstr(c) ] -> [ mk_rpattern (T (mk_lterm c None)) ]
+ | [ "in" lconstr(c) ] -> [ mk_rpattern (In_T (mk_lterm c None)) ]
+ | [ lconstr(x) "in" lconstr(c) ] ->
+ [ mk_rpattern (X_In_T (mk_lterm x None, mk_lterm c None)) ]
+ | [ "in" lconstr(x) "in" lconstr(c) ] ->
+ [ mk_rpattern (In_X_In_T (mk_lterm x None, mk_lterm c None)) ]
+ | [ lconstr(e) "in" lconstr(x) "in" lconstr(c) ] ->
+ [ mk_rpattern (E_In_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None)) ]
+ | [ lconstr(e) "as" lconstr(x) "in" lconstr(c) ] ->
+ [ mk_rpattern (E_As_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None)) ]
+END
+
+let pr_ssrterm _ _ _ = pr_ssrterm
+
+ARGUMENT EXTEND cpattern
+ PRINTED BY pr_ssrterm
+ INTERPRETED BY interp_ssrterm
+ GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm
+ RAW_PRINTED BY pr_ssrterm
+ GLOB_PRINTED BY pr_ssrterm
+| [ "Qed" constr(c) ] -> [ mk_lterm c None ]
+END
+
+let input_ssrtermkind strm = match Util.stream_nth 0 strm with
+ | Tok.KEYWORD "(" -> '('
+ | Tok.KEYWORD "@" -> '@'
+ | _ -> ' '
+let ssrtermkind = Pcoq.Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind
+
+GEXTEND Gram
+ GLOBAL: cpattern;
+ cpattern: [[ k = ssrtermkind; c = constr ->
+ let pattern = mk_term k c None in
+ if loc_of_cpattern pattern <> Some !@loc && k = '('
+ then mk_term 'x' c None
+ else pattern ]];
+END
+
+ARGUMENT EXTEND lcpattern
+ TYPED AS cpattern
+ PRINTED BY pr_ssrterm
+ INTERPRETED BY interp_ssrterm
+ GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm
+ RAW_PRINTED BY pr_ssrterm
+ GLOB_PRINTED BY pr_ssrterm
+| [ "Qed" lconstr(c) ] -> [ mk_lterm c None ]
+END
+
+GEXTEND Gram
+ GLOBAL: lcpattern;
+ lcpattern: [[ k = ssrtermkind; c = lconstr ->
+ let pattern = mk_term k c None in
+ if loc_of_cpattern pattern <> Some !@loc && k = '('
+ then mk_term 'x' c None
+ else pattern ]];
+END
+
+ARGUMENT EXTEND ssrpatternarg TYPED AS rpattern PRINTED BY pr_rpattern
+| [ rpattern(pat) ] -> [ pat ]
+END
+
+TACTIC EXTEND ssrinstoftpat
+| [ "ssrinstancesoftpat" cpattern(arg) ] -> [ Proofview.V82.tactic (ssrinstancesof arg) ]
+END
+
+(* We wipe out all the keywords generated by the grammar rules we defined. *)
+(* The user is supposed to Require Import ssreflect or Require ssreflect *)
+(* and Import ssreflect.SsrSyntax to obtain these keywords and as a *)
+(* consequence the extended ssreflect grammar. *)
+let () = CLexer.set_keyword_state frozen_lexer ;;
diff --git a/plugins/ssrmatching/g_ssrmatching.mli b/plugins/ssrmatching/g_ssrmatching.mli
new file mode 100644
index 0000000000..bb5161a0e0
--- /dev/null
+++ b/plugins/ssrmatching/g_ssrmatching.mli
@@ -0,0 +1,17 @@
+(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* Distributed under the terms of CeCILL-B. *)
+
+open Genarg
+open Ssrmatching
+
+(** CS cpattern: (f _), (X in t), (t in X in t), (t as X in t) *)
+val cpattern : cpattern Pcoq.Gram.entry
+val wit_cpattern : cpattern uniform_genarg_type
+
+(** OS cpattern: f _, (X in t), (t in X in t), (t as X in t) *)
+val lcpattern : cpattern Pcoq.Gram.entry
+val wit_lcpattern : cpattern uniform_genarg_type
+
+(** OS rpattern: f _, in t, X in t, in X in t, t in X in t, t as X in t *)
+val rpattern : rpattern Pcoq.Gram.entry
+val wit_rpattern : rpattern uniform_genarg_type
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml
index 9d9b1b2e8c..05eda14e90 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -10,10 +10,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-(* Defining grammar rules with "xx" in it automatically declares keywords too,
- * we thus save the lexer to restore it at the end of the file *)
-let frozen_lexer = CLexer.get_keyword_state () ;;
-
open Ltac_plugin
open Names
open Pp
@@ -22,8 +18,6 @@ open Stdarg
open Term
module CoqConstr = Constr
open CoqConstr
-open Pcoq
-open Pcoq.Constr
open Vars
open Libnames
open Tactics
@@ -46,8 +40,6 @@ open Evar_kinds
open Constrexpr
open Constrexpr_ops
-DECLARE PLUGIN "ssrmatching_plugin"
-
let errorstrm = CErrors.user_err ~hdr:"ssrmatching"
let loc_error loc msg = CErrors.user_err ?loc ~hdr:msg (str msg)
let ppnl = Feedback.msg_info
@@ -907,7 +899,6 @@ let pr_pattern_aux pr_constr = function
let pp_pattern (sigma, p) =
pr_pattern_aux (fun t -> pr_constr_pat (EConstr.Unsafe.to_constr (pi3 (nf_open_term sigma sigma (EConstr.of_constr t))))) p
let pr_cpattern = pr_term
-let pr_rpattern _ _ _ = pr_pattern
let wit_rpatternty = add_genarg "rpatternty" pr_pattern
@@ -987,27 +978,7 @@ let interp_rpattern s = function
| E_As_X_In_T(e,x,t) ->
E_As_X_In_T (interp_ssrterm s e,interp_ssrterm s x,interp_ssrterm s t)
-let interp_rpattern ist gl t = Tacmach.project gl, interp_rpattern ist t
-
-ARGUMENT EXTEND rpattern
- TYPED AS rpatternty
- PRINTED BY pr_rpattern
- INTERPRETED BY interp_rpattern
- GLOBALIZED BY glob_rpattern
- SUBSTITUTED BY subst_rpattern
- | [ lconstr(c) ] -> [ T (mk_lterm c None) ]
- | [ "in" lconstr(c) ] -> [ In_T (mk_lterm c None) ]
- | [ lconstr(x) "in" lconstr(c) ] ->
- [ X_In_T (mk_lterm x None, mk_lterm c None) ]
- | [ "in" lconstr(x) "in" lconstr(c) ] ->
- [ In_X_In_T (mk_lterm x None, mk_lterm c None) ]
- | [ lconstr(e) "in" lconstr(x) "in" lconstr(c) ] ->
- [ E_In_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None) ]
- | [ lconstr(e) "as" lconstr(x) "in" lconstr(c) ] ->
- [ E_As_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None) ]
-END
-
-
+let interp_rpattern0 ist gl t = Tacmach.project gl, interp_rpattern ist t
type cpattern = char * glob_constr_and_expr * Geninterp.interp_sign option
let tag_of_cpattern = pi1
@@ -1051,52 +1022,9 @@ let interp_wit wit ist gl x =
let interp_open_constr ist gl gc =
interp_wit wit_open_constr ist gl gc
let pf_intern_term gl (_, c, ist) = glob_constr ist (pf_env gl) (project gl) c
-let pr_ssrterm _ _ _ = pr_term
-let input_ssrtermkind strm = match stream_nth 0 strm with
- | Tok.KEYWORD "(" -> '('
- | Tok.KEYWORD "@" -> '@'
- | _ -> ' '
-let ssrtermkind = Pcoq.Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind
let interp_ssrterm ist gl t = Tacmach.project gl, interp_ssrterm ist t
-ARGUMENT EXTEND cpattern
- PRINTED BY pr_ssrterm
- INTERPRETED BY interp_ssrterm
- GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm
- RAW_PRINTED BY pr_ssrterm
- GLOB_PRINTED BY pr_ssrterm
-| [ "Qed" constr(c) ] -> [ mk_lterm c None ]
-END
-
-GEXTEND Gram
- GLOBAL: cpattern;
- cpattern: [[ k = ssrtermkind; c = constr ->
- let pattern = mk_term k c None in
- if loc_ofCG pattern <> Some !@loc && k = '('
- then mk_term 'x' c None
- else pattern ]];
-END
-
-ARGUMENT EXTEND lcpattern
- TYPED AS cpattern
- PRINTED BY pr_ssrterm
- INTERPRETED BY interp_ssrterm
- GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm
- RAW_PRINTED BY pr_ssrterm
- GLOB_PRINTED BY pr_ssrterm
-| [ "Qed" lconstr(c) ] -> [ mk_lterm c None ]
-END
-
-GEXTEND Gram
- GLOBAL: lcpattern;
- lcpattern: [[ k = ssrtermkind; c = lconstr ->
- let pattern = mk_term k c None in
- if loc_ofCG pattern <> Some !@loc && k = '('
- then mk_term 'x' c None
- else pattern ]];
-END
-
let interp_term gl = function
| (_, c, Some ist) ->
on_snd EConstr.Unsafe.to_constr (interp_open_constr ist gl c)
@@ -1416,10 +1344,6 @@ let is_wildcard ((_, (l, r), _) : cpattern) : bool = match DAst.get l, r with
(* "ssrpattern" *)
-ARGUMENT EXTEND ssrpatternarg TYPED AS rpattern PRINTED BY pr_rpattern
-| [ rpattern(pat) ] -> [ pat ]
-END
-
let pr_rpattern = pr_pattern
let pf_merge_uc uc gl =
@@ -1428,6 +1352,9 @@ let pf_merge_uc uc gl =
let pf_unsafe_merge_uc uc gl =
re_sig (sig_it gl) (Evd.set_universe_context (project gl) uc)
+(** All the pattern types reuse the same dynamic toplevel tag *)
+let wit_ssrpatternarg = wit_rpatternty
+
let interp_rpattern = interp_rpattern ~wit_ssrpatternarg
let ssrpatterntac _ist arg gl =
@@ -1479,14 +1406,20 @@ let ssrinstancesof arg gl =
done; raise NoMatch
with NoMatch -> ppnl (str"END INSTANCES"); tclIDTAC gl
-TACTIC EXTEND ssrinstoftpat
-| [ "ssrinstancesoftpat" cpattern(arg) ] -> [ Proofview.V82.tactic (ssrinstancesof arg) ]
-END
-
-(* We wipe out all the keywords generated by the grammar rules we defined. *)
-(* The user is supposed to Require Import ssreflect or Require ssreflect *)
-(* and Import ssreflect.SsrSyntax to obtain these keywords and as a *)
-(* consequence the extended ssreflect grammar. *)
-let () = CLexer.set_keyword_state frozen_lexer ;;
+module Internal =
+struct
+ let wit_rpatternty = wit_rpatternty
+ let glob_rpattern = glob_rpattern
+ let subst_rpattern = subst_rpattern
+ let interp_rpattern = interp_rpattern0
+ let pr_rpattern = pr_rpattern
+ let mk_rpattern x = x
+ let mk_lterm = mk_lterm
+ let mk_term = mk_term
+ let glob_cpattern = glob_cpattern
+ let subst_ssrterm = subst_ssrterm
+ let interp_ssrterm = interp_ssrterm
+ let pr_ssrterm = pr_term
+end
(* vim: set filetype=ocaml foldmethod=marker: *)
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index c55081e0f7..f478d48ea3 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -2,7 +2,6 @@
(* Distributed under the terms of CeCILL-B. *)
open Goal
-open Genarg
open Environ
open Evd
open Constr
@@ -19,24 +18,12 @@ open Tacexpr
type cpattern
val pr_cpattern : cpattern -> Pp.t
-(** CS cpattern: (f _), (X in t), (t in X in t), (t as X in t) *)
-val cpattern : cpattern Pcoq.Gram.entry
-val wit_cpattern : cpattern uniform_genarg_type
-
-(** OS cpattern: f _, (X in t), (t in X in t), (t as X in t) *)
-val lcpattern : cpattern Pcoq.Gram.entry
-val wit_lcpattern : cpattern uniform_genarg_type
-
(** The type of rewrite patterns, the patterns of the [rewrite] tactic.
These patterns also include patterns that identify all the subterms
of a context (i.e. "in" prefix) *)
type rpattern
val pr_rpattern : rpattern -> Pp.t
-(** OS rpattern: f _, in t, X in t, in X in t, t in X in t, t as X in t *)
-val rpattern : rpattern Pcoq.Gram.entry
-val wit_rpattern : rpattern uniform_genarg_type
-
(** Pattern interpretation and matching *)
exception NoMatch
@@ -238,4 +225,25 @@ val debug : bool -> unit
* "Unset SsrMatchingProfiling" to get timings *)
val profile : bool -> unit
+val ssrinstancesof : cpattern -> Tacmach.tactic
+
+(** Functions used for grammar extensions. Do not use. *)
+
+module Internal :
+sig
+ val wit_rpatternty : (rpattern, rpattern, rpattern) Genarg.genarg_type
+ val glob_rpattern : Genintern.glob_sign -> rpattern -> rpattern
+ val subst_rpattern : Mod_subst.substitution -> rpattern -> rpattern
+ val interp_rpattern : Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> rpattern -> Evd.evar_map * rpattern
+ val pr_rpattern : rpattern -> Pp.t
+ val mk_rpattern : (cpattern, cpattern) ssrpattern -> rpattern
+ val mk_lterm : Constrexpr.constr_expr -> Geninterp.interp_sign option -> cpattern
+ val mk_term : char -> Constrexpr.constr_expr -> Geninterp.interp_sign option -> cpattern
+
+ val glob_cpattern : Genintern.glob_sign -> cpattern -> cpattern
+ val subst_ssrterm : Mod_subst.substitution -> cpattern -> cpattern
+ val interp_ssrterm : Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> cpattern -> Evd.evar_map * cpattern
+ val pr_ssrterm : cpattern -> Pp.t
+end
+
(* eof *)
diff --git a/plugins/ssrmatching/ssrmatching_plugin.mlpack b/plugins/ssrmatching/ssrmatching_plugin.mlpack
index 5fb1f1567d..02c75f14ed 100644
--- a/plugins/ssrmatching/ssrmatching_plugin.mlpack
+++ b/plugins/ssrmatching/ssrmatching_plugin.mlpack
@@ -1 +1,2 @@
Ssrmatching
+G_ssrmatching
diff --git a/plugins/syntax/n_syntax.ml b/plugins/syntax/n_syntax.ml
new file mode 100644
index 0000000000..0e202be47f
--- /dev/null
+++ b/plugins/syntax/n_syntax.ml
@@ -0,0 +1,81 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Pp
+open CErrors
+open Names
+open Bigint
+open Positive_syntax_plugin.Positive_syntax
+
+(* Poor's man DECLARE PLUGIN *)
+let __coq_plugin_name = "n_syntax_plugin"
+let () = Mltop.add_known_module __coq_plugin_name
+
+(**********************************************************************)
+(* Parsing N via scopes *)
+(**********************************************************************)
+
+open Globnames
+open Glob_term
+
+let binnums = ["Coq";"Numbers";"BinNums"]
+
+let make_dir l = DirPath.make (List.rev_map Id.of_string l)
+let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
+
+(* TODO: temporary hack *)
+let make_kn dir id = Globnames.encode_mind dir id
+
+let n_kn = make_kn (make_dir binnums) (Id.of_string "N")
+let glob_n = IndRef (n_kn,0)
+let path_of_N0 = ((n_kn,0),1)
+let path_of_Npos = ((n_kn,0),2)
+let glob_N0 = ConstructRef path_of_N0
+let glob_Npos = ConstructRef path_of_Npos
+
+let n_path = make_path binnums "N"
+
+let n_of_binnat ?loc pos_or_neg n = DAst.make ?loc @@
+ if not (Bigint.equal n zero) then
+ GApp(DAst.make @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n])
+ else
+ GRef(glob_N0, None)
+
+let error_negative ?loc =
+ user_err ?loc ~hdr:"interp_N" (str "No negative numbers in type \"N\".")
+
+let n_of_int ?loc n =
+ if is_pos_or_zero n then n_of_binnat ?loc true n
+ else error_negative ?loc
+
+(**********************************************************************)
+(* Printing N via scopes *)
+(**********************************************************************)
+
+let bignat_of_n n = DAst.with_val (function
+ | GApp (r, [a]) when is_gr r glob_Npos -> bignat_of_pos a
+ | GRef (a,_) when GlobRef.equal a glob_N0 -> Bigint.zero
+ | _ -> raise Non_closed_number
+ ) n
+
+let uninterp_n (AnyGlobConstr p) =
+ try Some (bignat_of_n p)
+ with Non_closed_number -> None
+
+(************************************************************************)
+(* Declaring interpreters and uninterpreters for N *)
+
+let _ = Notation.declare_numeral_interpreter "N_scope"
+ (n_path,binnums)
+ n_of_int
+ ([DAst.make @@ GRef (glob_N0, None);
+ DAst.make @@ GRef (glob_Npos, None)],
+ uninterp_n,
+ true)
diff --git a/plugins/syntax/n_syntax_plugin.mlpack b/plugins/syntax/n_syntax_plugin.mlpack
new file mode 100644
index 0000000000..4c56645f07
--- /dev/null
+++ b/plugins/syntax/n_syntax_plugin.mlpack
@@ -0,0 +1 @@
+N_syntax
diff --git a/plugins/syntax/positive_syntax.ml b/plugins/syntax/positive_syntax.ml
new file mode 100644
index 0000000000..0c82e47445
--- /dev/null
+++ b/plugins/syntax/positive_syntax.ml
@@ -0,0 +1,101 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Pp
+open CErrors
+open Util
+open Names
+open Bigint
+
+(* Poor's man DECLARE PLUGIN *)
+let __coq_plugin_name = "positive_syntax_plugin"
+let () = Mltop.add_known_module __coq_plugin_name
+
+exception Non_closed_number
+
+(**********************************************************************)
+(* Parsing positive via scopes *)
+(**********************************************************************)
+
+open Globnames
+open Glob_term
+
+let binnums = ["Coq";"Numbers";"BinNums"]
+
+let make_dir l = DirPath.make (List.rev_map Id.of_string l)
+let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
+
+let positive_path = make_path binnums "positive"
+
+(* TODO: temporary hack *)
+let make_kn dir id = Globnames.encode_mind dir id
+
+let positive_kn = make_kn (make_dir binnums) (Id.of_string "positive")
+let glob_positive = IndRef (positive_kn,0)
+let path_of_xI = ((positive_kn,0),1)
+let path_of_xO = ((positive_kn,0),2)
+let path_of_xH = ((positive_kn,0),3)
+let glob_xI = ConstructRef path_of_xI
+let glob_xO = ConstructRef path_of_xO
+let glob_xH = ConstructRef path_of_xH
+
+let pos_of_bignat ?loc x =
+ let ref_xI = DAst.make ?loc @@ GRef (glob_xI, None) in
+ let ref_xH = DAst.make ?loc @@ GRef (glob_xH, None) in
+ let ref_xO = DAst.make ?loc @@ GRef (glob_xO, None) in
+ let rec pos_of x =
+ match div2_with_rest x with
+ | (q,false) -> DAst.make ?loc @@ GApp (ref_xO,[pos_of q])
+ | (q,true) when not (Bigint.equal q zero) -> DAst.make ?loc @@ GApp (ref_xI,[pos_of q])
+ | (q,true) -> ref_xH
+ in
+ pos_of x
+
+let error_non_positive ?loc =
+ user_err ?loc ~hdr:"interp_positive"
+ (str "Only strictly positive numbers in type \"positive\".")
+
+let interp_positive ?loc n =
+ if is_strictly_pos n then pos_of_bignat ?loc n
+ else error_non_positive ?loc
+
+(**********************************************************************)
+(* Printing positive via scopes *)
+(**********************************************************************)
+
+let is_gr c gr = match DAst.get c with
+| GRef (r, _) -> GlobRef.equal r gr
+| _ -> false
+
+let rec bignat_of_pos x = DAst.with_val (function
+ | GApp (r ,[a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a)
+ | GApp (r ,[a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a))
+ | GRef (a, _) when GlobRef.equal a glob_xH -> Bigint.one
+ | _ -> raise Non_closed_number
+ ) x
+
+let uninterp_positive (AnyGlobConstr p) =
+ try
+ Some (bignat_of_pos p)
+ with Non_closed_number ->
+ None
+
+(************************************************************************)
+(* Declaring interpreters and uninterpreters for positive *)
+(************************************************************************)
+
+let _ = Notation.declare_numeral_interpreter "positive_scope"
+ (positive_path,binnums)
+ interp_positive
+ ([DAst.make @@ GRef (glob_xI, None);
+ DAst.make @@ GRef (glob_xO, None);
+ DAst.make @@ GRef (glob_xH, None)],
+ uninterp_positive,
+ true)
diff --git a/plugins/syntax/positive_syntax_plugin.mlpack b/plugins/syntax/positive_syntax_plugin.mlpack
new file mode 100644
index 0000000000..ac8f3c425c
--- /dev/null
+++ b/plugins/syntax/positive_syntax_plugin.mlpack
@@ -0,0 +1 @@
+Positive_syntax
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index 09fe8bf70a..2534162e36 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -8,20 +8,16 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Pp
-open CErrors
-open Util
open Names
open Bigint
+open Positive_syntax_plugin.Positive_syntax
(* Poor's man DECLARE PLUGIN *)
let __coq_plugin_name = "z_syntax_plugin"
let () = Mltop.add_known_module __coq_plugin_name
-exception Non_closed_number
-
(**********************************************************************)
-(* Parsing positive via scopes *)
+(* Parsing Z via scopes *)
(**********************************************************************)
open Globnames
@@ -32,129 +28,9 @@ let binnums = ["Coq";"Numbers";"BinNums"]
let make_dir l = DirPath.make (List.rev_map Id.of_string l)
let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
-let positive_path = make_path binnums "positive"
-
(* TODO: temporary hack *)
let make_kn dir id = Globnames.encode_mind dir id
-let positive_kn = make_kn (make_dir binnums) (Id.of_string "positive")
-let glob_positive = IndRef (positive_kn,0)
-let path_of_xI = ((positive_kn,0),1)
-let path_of_xO = ((positive_kn,0),2)
-let path_of_xH = ((positive_kn,0),3)
-let glob_xI = ConstructRef path_of_xI
-let glob_xO = ConstructRef path_of_xO
-let glob_xH = ConstructRef path_of_xH
-
-let pos_of_bignat ?loc x =
- let ref_xI = DAst.make ?loc @@ GRef (glob_xI, None) in
- let ref_xH = DAst.make ?loc @@ GRef (glob_xH, None) in
- let ref_xO = DAst.make ?loc @@ GRef (glob_xO, None) in
- let rec pos_of x =
- match div2_with_rest x with
- | (q,false) -> DAst.make ?loc @@ GApp (ref_xO,[pos_of q])
- | (q,true) when not (Bigint.equal q zero) -> DAst.make ?loc @@ GApp (ref_xI,[pos_of q])
- | (q,true) -> ref_xH
- in
- pos_of x
-
-let error_non_positive ?loc =
- user_err ?loc ~hdr:"interp_positive"
- (str "Only strictly positive numbers in type \"positive\".")
-
-let interp_positive ?loc n =
- if is_strictly_pos n then pos_of_bignat ?loc n
- else error_non_positive ?loc
-
-(**********************************************************************)
-(* Printing positive via scopes *)
-(**********************************************************************)
-
-let is_gr c gr = match DAst.get c with
-| GRef (r, _) -> GlobRef.equal r gr
-| _ -> false
-
-let rec bignat_of_pos x = DAst.with_val (function
- | GApp (r ,[a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a)
- | GApp (r ,[a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a))
- | GRef (a, _) when GlobRef.equal a glob_xH -> Bigint.one
- | _ -> raise Non_closed_number
- ) x
-
-let uninterp_positive (AnyGlobConstr p) =
- try
- Some (bignat_of_pos p)
- with Non_closed_number ->
- None
-
-(************************************************************************)
-(* Declaring interpreters and uninterpreters for positive *)
-(************************************************************************)
-
-let _ = Notation.declare_numeral_interpreter "positive_scope"
- (positive_path,binnums)
- interp_positive
- ([DAst.make @@ GRef (glob_xI, None);
- DAst.make @@ GRef (glob_xO, None);
- DAst.make @@ GRef (glob_xH, None)],
- uninterp_positive,
- true)
-
-(**********************************************************************)
-(* Parsing N via scopes *)
-(**********************************************************************)
-
-let n_kn = make_kn (make_dir binnums) (Id.of_string "N")
-let glob_n = IndRef (n_kn,0)
-let path_of_N0 = ((n_kn,0),1)
-let path_of_Npos = ((n_kn,0),2)
-let glob_N0 = ConstructRef path_of_N0
-let glob_Npos = ConstructRef path_of_Npos
-
-let n_path = make_path binnums "N"
-
-let n_of_binnat ?loc pos_or_neg n = DAst.make ?loc @@
- if not (Bigint.equal n zero) then
- GApp(DAst.make @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n])
- else
- GRef(glob_N0, None)
-
-let error_negative ?loc =
- user_err ?loc ~hdr:"interp_N" (str "No negative numbers in type \"N\".")
-
-let n_of_int ?loc n =
- if is_pos_or_zero n then n_of_binnat ?loc true n
- else error_negative ?loc
-
-(**********************************************************************)
-(* Printing N via scopes *)
-(**********************************************************************)
-
-let bignat_of_n n = DAst.with_val (function
- | GApp (r, [a]) when is_gr r glob_Npos -> bignat_of_pos a
- | GRef (a,_) when GlobRef.equal a glob_N0 -> Bigint.zero
- | _ -> raise Non_closed_number
- ) n
-
-let uninterp_n (AnyGlobConstr p) =
- try Some (bignat_of_n p)
- with Non_closed_number -> None
-
-(************************************************************************)
-(* Declaring interpreters and uninterpreters for N *)
-
-let _ = Notation.declare_numeral_interpreter "N_scope"
- (n_path,binnums)
- n_of_int
- ([DAst.make @@ GRef (glob_N0, None);
- DAst.make @@ GRef (glob_Npos, None)],
- uninterp_n,
- true)
-
-(**********************************************************************)
-(* Parsing Z via scopes *)
-(**********************************************************************)
-
let z_path = make_path binnums "Z"
let z_kn = make_kn (make_dir binnums) (Id.of_string "Z")
let glob_z = IndRef (z_kn,0)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 16:13:36 +0000