aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_tactic.ml416
-rw-r--r--parsing/pcoq.mli2
-rw-r--r--parsing/pptactic.ml14
-rw-r--r--parsing/pptactic.mli1
-rw-r--r--parsing/ppvernac.ml4
-rw-r--r--parsing/q_coqast.ml48
6 files changed, 30 insertions, 15 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 3cbd12e53..34cdd44d6 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -158,6 +158,10 @@ GEXTEND Gram
| c1 = constr; "at"; nl = LIST1 int_or_var; "with"; c2 = constr ->
(Some (nl,c1), c2) ] ]
;
+ smart_global:
+ [ [ c = global -> AN c
+ | s = ne_string -> ByNotation (loc,s) ] ]
+ ;
occurrences:
[ [ "at"; nl = LIST1 int_or_var -> nl
| -> [] ] ]
@@ -166,7 +170,7 @@ GEXTEND Gram
[ [ c = constr; nl = occurrences -> (nl,c) ] ]
;
unfold_occ:
- [ [ c = global; nl = occurrences -> (nl,c) ] ]
+ [ [ c = smart_global; nl = occurrences -> (nl,c) ] ]
;
intropatterns:
[ [ l = LIST0 simple_intropattern -> l ]]
@@ -200,14 +204,14 @@ GEXTEND Gram
| IDENT "delta" -> FDeltaBut []
| IDENT "iota" -> FIota
| IDENT "zeta" -> FZeta
- | IDENT "delta"; "["; idl = LIST1 global; "]" -> FConst idl
- | IDENT "delta"; "-"; "["; idl = LIST1 global; "]" -> FDeltaBut idl
+ | IDENT "delta"; "["; idl = LIST1 smart_global; "]" -> FConst idl
+ | IDENT "delta"; "-"; "["; idl = LIST1 smart_global; "]" -> FDeltaBut idl
] ]
;
delta_flag:
- [ [ IDENT "delta"; "["; idl = LIST1 global; "]" -> FConst idl
- | IDENT "delta"; "-"; "["; idl = LIST1 global; "]" -> FDeltaBut idl
+ [ [ IDENT "delta"; "["; idl = LIST1 smart_global; "]" -> FConst idl
+ | IDENT "delta"; "-"; "["; idl = LIST1 smart_global; "]" -> FDeltaBut idl
] ]
;
@@ -379,7 +383,7 @@ GEXTEND Gram
el = OPT eliminator -> TacNewDestruct (lc,el,ids)
| IDENT "decompose"; IDENT "record" ; c = constr -> TacDecomposeAnd c
| IDENT "decompose"; IDENT "sum"; c = constr -> TacDecomposeOr c
- | IDENT "decompose"; "["; l = LIST1 global; "]"; c = constr
+ | IDENT "decompose"; "["; l = LIST1 smart_global; "]"; c = constr
-> TacDecompose (l,c)
(* Automation tactic *)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index a79727539..523ad92fb 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -176,7 +176,7 @@ module Tactic :
val casted_open_constr : open_constr_expr Gram.Entry.e
val constr_with_bindings : constr_expr with_bindings Gram.Entry.e
val bindings : constr_expr bindings Gram.Entry.e
- val constr_may_eval : (constr_expr,reference) may_eval Gram.Entry.e
+ val constr_may_eval : (constr_expr,reference or_by_notation) may_eval Gram.Entry.e
val quantified_hypothesis : quantified_hypothesis Gram.Entry.e
val int_or_var : int or_var Gram.Entry.e
val red_expr : raw_red_expr Gram.Entry.e
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 9218fb816..b6c38cf93 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -77,6 +77,10 @@ let pr_or_metaid pr = function
let pr_and_short_name pr (c,_) = pr c
+let pr_or_by_notation f = function
+ | AN v -> f v
+ | ByNotation (_,s) -> str s
+
let pr_located pr (loc,x) = pr x
let pr_evaluable_reference = function
@@ -144,11 +148,13 @@ let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel Genarg.generic_argu
| SortArgType -> pr_arg pr_rawsort (out_gen rawwit_sort x)
| ConstrArgType -> pr_arg prc (out_gen rawwit_constr x)
| ConstrMayEvalArgType ->
- pr_arg (pr_may_eval prc prlc prref) (out_gen rawwit_constr_may_eval x)
+ pr_arg (pr_may_eval prc prlc (pr_or_by_notation prref))
+ (out_gen rawwit_constr_may_eval x)
| QuantHypArgType ->
pr_arg pr_quantified_hypothesis (out_gen rawwit_quant_hyp x)
| RedExprArgType ->
- pr_arg (pr_red_expr (prc,prlc,prref)) (out_gen rawwit_red_expr x)
+ pr_arg (pr_red_expr (prc,prlc,pr_or_by_notation prref))
+ (out_gen rawwit_red_expr x)
| OpenConstrArgType b -> pr_arg prc (snd (out_gen (rawwit_open_constr_gen b) x))
| ConstrWithBindingsArgType ->
pr_arg (pr_with_bindings prc prlc) (out_gen rawwit_constr_with_bindings x)
@@ -976,8 +982,8 @@ let rec raw_printers =
drop_env pr_constr_expr,
drop_env pr_lconstr_expr,
pr_lpattern_expr,
- drop_env pr_reference,
- drop_env pr_reference,
+ drop_env (pr_or_by_notation pr_reference),
+ drop_env (pr_or_by_notation pr_reference),
pr_reference,
pr_or_metaid pr_lident,
pr_raw_extend,
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index 993f1ae62..cfa035b16 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -21,6 +21,7 @@ open Environ
val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
val pr_or_metaid : ('a -> std_ppcmds) -> 'a or_metaid -> std_ppcmds
val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds
+val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds
type 'a raw_extra_genarg_printer =
(constr_expr -> std_ppcmds) ->
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index c2571ad0a..9b0186368 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -484,7 +484,7 @@ let rec pr_vernac = function
| None -> mt()
| Some r ->
str"Eval" ++ spc() ++
- pr_red_expr (pr_constr, pr_lconstr, pr_reference) r ++
+ pr_red_expr (pr_constr, pr_lconstr, pr_or_by_notation pr_reference) r ++
str" in" ++ spc() in
let pr_def_body = function
| DefineBody (bl,red,body,d) ->
@@ -776,7 +776,7 @@ let rec pr_vernac = function
let pr_mayeval r c = match r with
| Some r0 ->
hov 2 (str"Eval" ++ spc() ++
- pr_red_expr (pr_constr,pr_lconstr,pr_reference) r0 ++
+ pr_red_expr (pr_constr,pr_lconstr,pr_or_by_notation pr_reference) r0 ++
spc() ++ str"in" ++ spc () ++ pr_constr c)
| None -> hov 2 (str"Check" ++ spc() ++ pr_constr c)
in
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index ef25e9b8d..a8c975eb1 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -55,6 +55,10 @@ let mlexpr_of_reference = function
| Libnames.Qualid (loc,qid) -> <:expr< Libnames.Qualid $dloc$ $mlexpr_of_qualid qid$ >>
| Libnames.Ident (loc,id) -> <:expr< Libnames.Ident $dloc$ $mlexpr_of_ident id$ >>
+let mlexpr_of_by_notation f = function
+ | Genarg.AN x -> <:expr< Genarg.AN $f x$ >>
+ | Genarg.ByNotation (loc,s) -> <:expr< Genarg.ByNotation $dloc$ $str:s$ >>
+
let mlexpr_of_intro_pattern = function
| Genarg.IntroOrAndPattern _ -> failwith "mlexpr_of_intro_pattern: TODO"
| Genarg.IntroWildcard -> <:expr< Genarg.IntroWildcard >>
@@ -112,7 +116,7 @@ let mlexpr_of_red_flags {
Rawterm.rIota = $mlexpr_of_bool bi$;
Rawterm.rZeta = $mlexpr_of_bool bz$;
Rawterm.rDelta = $mlexpr_of_bool bd$;
- Rawterm.rConst = $mlexpr_of_list mlexpr_of_reference l$
+ Rawterm.rConst = $mlexpr_of_list (mlexpr_of_by_notation mlexpr_of_reference) l$
} >>
let mlexpr_of_explicitation = function
@@ -155,7 +159,7 @@ let mlexpr_of_red_expr = function
<:expr< Rawterm.Lazy $mlexpr_of_red_flags f$ >>
| Rawterm.Unfold l ->
let f1 = mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int) in
- let f2 = mlexpr_of_reference in
+ let f2 = mlexpr_of_by_notation mlexpr_of_reference in
let f = mlexpr_of_list (mlexpr_of_pair f1 f2) in
<:expr< Rawterm.Unfold $f l$ >>
| Rawterm.Fold l ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 01:10:05 +0000