aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrequality.ml2
-rw-r--r--plugins/ssr/ssrparser.mlg53
-rw-r--r--plugins/ssr/ssrprinters.ml9
-rw-r--r--plugins/ssr/ssrvernac.mlg8
4 files changed, 38 insertions, 34 deletions
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 38b26d06b9..a7ebd5f9f5 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -240,7 +240,7 @@ let strip_unfold_term _ ((sigma, t) as p) kt = match EConstr.kind sigma t with
let same_proj sigma t1 t2 =
match EConstr.kind sigma t1, EConstr.kind sigma t2 with
- | Proj(c1,_), Proj(c2, _) -> Projection.equal c1 c2
+ | Proj(c1,_), Proj(c2, _) -> Projection.CanOrd.equal c1 c2
| _ -> false
let all_ok _ _ = true
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 7b584b5159..35fecfb0a5 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -100,7 +100,7 @@ ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma }
END
GRAMMAR EXTEND Gram
GLOBAL: ssrtacarg;
- ssrtacarg: [[ tac = tactic_expr LEVEL "5" -> { tac } ]];
+ ssrtacarg: [[ tac = ltac_expr LEVEL "5" -> { tac } ]];
END
(* Copy of ssrtacarg with LEVEL "3", useful for: "under ... do ..." *)
@@ -108,7 +108,7 @@ ARGUMENT EXTEND ssrtac3arg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma }
END
GRAMMAR EXTEND Gram
GLOBAL: ssrtac3arg;
- ssrtac3arg: [[ tac = tactic_expr LEVEL "3" -> { tac } ]];
+ ssrtac3arg: [[ tac = ltac_expr LEVEL "3" -> { tac } ]];
END
{
@@ -1337,7 +1337,7 @@ ARGUMENT EXTEND ssrbinder TYPED AS (ssrfwdfmt * constr) PRINTED BY { pr_ssrbinde
GRAMMAR EXTEND Gram
GLOBAL: ssrbinder;
ssrbinder: [
- [ ["of" -> { () } | "&" -> { () } ]; c = operconstr LEVEL "99" -> {
+ [ ["of" -> { () } | "&" -> { () } ]; c = term LEVEL "99" -> {
(FwdPose, [BFvar]),
CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Glob_term.Explicit,c)],mkCHole (Some loc)) } ]
];
@@ -1594,18 +1594,18 @@ GRAMMAR EXTEND Gram
| n = Prim.natural -> { ArgArg (check_index ~loc n) }
] ];
ssrswap: [[ IDENT "first" -> { loc, true } | IDENT "last" -> { loc, false } ]];
- ssrorelse: [[ "||"; tac = tactic_expr LEVEL "2" -> { tac } ]];
+ ssrorelse: [[ "||"; tac = ltac_expr LEVEL "2" -> { tac } ]];
ssrseqarg: [
[ arg = ssrswap -> { noindex, swaptacarg arg }
| i = ssrseqidx; tac = ssrortacarg; def = OPT ssrorelse -> { i, (tac, def) }
| i = ssrseqidx; arg = ssrswap -> { i, swaptacarg arg }
- | tac = tactic_expr LEVEL "3" -> { noindex, (mk_hint tac, None) }
+ | tac = ltac_expr LEVEL "3" -> { noindex, (mk_hint tac, None) }
] ];
END
{
-let tactic_expr = Pltac.tactic_expr
+let ltac_expr = Pltac.ltac_expr
}
@@ -1688,9 +1688,9 @@ let tclintros_expr ?loc tac ipats =
}
GRAMMAR EXTEND Gram
- GLOBAL: tactic_expr;
- tactic_expr: LEVEL "1" [ RIGHTA
- [ tac = tactic_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros }
+ GLOBAL: ltac_expr;
+ ltac_expr: LEVEL "1" [ RIGHTA
+ [ tac = ltac_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros }
] ];
END
@@ -1704,9 +1704,9 @@ END
(* (Removing user-specified parentheses is dubious anyway). *)
GRAMMAR EXTEND Gram
- GLOBAL: tactic_expr;
- ssrparentacarg: [[ "("; tac = tactic_expr; ")" -> { CAst.make ~loc (Tacexp tac) } ]];
- tactic_expr: LEVEL "0" [[ arg = ssrparentacarg -> { TacArg arg } ]];
+ GLOBAL: ltac_expr;
+ ssrparentacarg: [[ "("; tac = ltac_expr; ")" -> { CAst.make ~loc (Tacexp tac) } ]];
+ ltac_expr: LEVEL "0" [[ arg = ssrparentacarg -> { TacArg arg } ]];
END
(** The internal "done" and "ssrautoprop" tactics. *)
@@ -1741,7 +1741,7 @@ let tclBY tac = Tacticals.New.tclTHEN tac (donetac ~-1)
(* The latter two are used in forward-chaining tactics (have, suffice, wlog) *)
(* and subgoal reordering tacticals (; first & ; last), respectively. *)
-(* Force use of the tactic_expr parsing entry, to rule out tick marks. *)
+(* Force use of the ltac_expr parsing entry, to rule out tick marks. *)
(** The "by" tactical. *)
@@ -1782,12 +1782,12 @@ let ssrdotac_expr ?loc n m tac clauses =
}
GRAMMAR EXTEND Gram
- GLOBAL: tactic_expr;
+ GLOBAL: ltac_expr;
ssrdotac: [
- [ tac = tactic_expr LEVEL "3" -> { mk_hint tac }
+ [ tac = ltac_expr LEVEL "3" -> { mk_hint tac }
| tacs = ssrortacarg -> { tacs }
] ];
- tactic_expr: LEVEL "3" [ RIGHTA
+ ltac_expr: LEVEL "3" [ RIGHTA
[ IDENT "do"; m = ssrmmod; tac = ssrdotac; clauses = ssrclauses ->
{ ssrdotac_expr ~loc noindex m tac clauses }
| IDENT "do"; tac = ssrortacarg; clauses = ssrclauses ->
@@ -1833,20 +1833,20 @@ let tclseq_expr ?loc tac dir arg =
}
GRAMMAR EXTEND Gram
- GLOBAL: tactic_expr;
+ GLOBAL: ltac_expr;
ssr_first: [
[ tac = ssr_first; ipats = ssrintros_ne -> { tclintros_expr ~loc tac ipats }
- | "["; tacl = LIST0 tactic_expr SEP "|"; "]" -> { TacFirst tacl }
+ | "["; tacl = LIST0 ltac_expr SEP "|"; "]" -> { TacFirst tacl }
] ];
ssr_first_else: [
[ tac1 = ssr_first; tac2 = ssrorelse -> { TacOrelse (tac1, tac2) }
| tac = ssr_first -> { tac } ]];
- tactic_expr: LEVEL "4" [ LEFTA
- [ tac1 = tactic_expr; ";"; IDENT "first"; tac2 = ssr_first_else ->
+ ltac_expr: LEVEL "4" [ LEFTA
+ [ tac1 = ltac_expr; ";"; IDENT "first"; tac2 = ssr_first_else ->
{ TacThen (tac1, tac2) }
- | tac = tactic_expr; ";"; IDENT "first"; arg = ssrseqarg ->
+ | tac = ltac_expr; ";"; IDENT "first"; arg = ssrseqarg ->
{ tclseq_expr ~loc tac L2R arg }
- | tac = tactic_expr; ";"; IDENT "last"; arg = ssrseqarg ->
+ | tac = ltac_expr; ";"; IDENT "last"; arg = ssrseqarg ->
{ tclseq_expr ~loc tac R2L arg }
] ];
END
@@ -1894,7 +1894,8 @@ let has_occ ((_, occ), _) = occ <> None
let gens_sep = function [], [] -> mt | _ -> spc
let pr_dgens pr_gen (gensl, clr) =
- let prgens s gens = str s ++ pr_list spc pr_gen gens in
+ let prgens s gens =
+ if CList.is_empty gens then mt () else str s ++ pr_list spc pr_gen gens in
let prdeps deps = prgens ": " deps ++ spc () ++ str "/" in
match gensl with
| [deps; []] -> prdeps deps ++ pr_clear pr_spc clr
@@ -2194,7 +2195,7 @@ END
let pr_ssrcongrarg _ _ _ ((n, f), dgens) =
(if n <= 0 then mt () else str " " ++ int n) ++
- str " " ++ pr_term f ++ pr_dgens pr_gen dgens
+ pr_term f ++ pr_dgens pr_gen dgens
}
@@ -2447,8 +2448,8 @@ END
(* The standard TACTIC EXTEND does not work for abstract *)
GRAMMAR EXTEND Gram
- GLOBAL: tactic_expr;
- tactic_expr: LEVEL "3"
+ GLOBAL: ltac_expr;
+ ltac_expr: LEVEL "3"
[ RIGHTA [ IDENT "abstract"; gens = ssrdgens ->
{ ssrtac_expr ~loc "abstract"
[Tacexpr.TacGeneric (None, Genarg.in_gen (Genarg.rawwit wit_ssrdgens) gens)] } ]];
diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml
index e231ab1f87..ab36d4fc7c 100644
--- a/plugins/ssr/ssrprinters.ml
+++ b/plugins/ssr/ssrprinters.ml
@@ -75,11 +75,14 @@ let pr_hyp (SsrHyp (_, id)) = Id.print id
let pr_hyps = pr_list pr_spc pr_hyp
let pr_occ = function
- | Some (true, occ) -> str "{-" ++ pr_list pr_spc int occ ++ str "}"
- | Some (false, occ) -> str "{+" ++ pr_list pr_spc int occ ++ str "}"
+ | Some (true, occ) ->
+ if CList.is_empty occ then mt () else str "{-" ++ pr_list pr_spc int occ ++ str "}"
+ | Some (false, occ) ->
+ if CList.is_empty occ then mt () else str "{+" ++ pr_list pr_spc int occ ++ str "}"
| None -> str "{}"
-let pr_clear_ne clr = str "{" ++ pr_hyps clr ++ str "}"
+let pr_clear_ne clr =
+ if CList.is_empty clr then mt () else str "{" ++ pr_hyps clr ++ str "}"
let pr_clear sep clr = sep () ++ pr_clear_ne clr
let pr_dir = function L2R -> str "->" | R2L -> str "<-"
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 91cd5b251c..a49a5e8b28 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -85,7 +85,7 @@ let mk_pat c (na, t) = (c, na, t)
GRAMMAR EXTEND Gram
GLOBAL: binder_constr;
- ssr_rtype: [[ "return"; t = operconstr LEVEL "100" -> { mk_rtype t } ]];
+ ssr_rtype: [[ "return"; t = term LEVEL "100" -> { mk_rtype t } ]];
ssr_mpat: [[ p = pattern -> { [[p]] } ]];
ssr_dpat: [
[ mp = ssr_mpat; "in"; t = pattern; rt = ssr_rtype -> { mp, mk_ctype mp t, rt }
@@ -96,9 +96,9 @@ GRAMMAR EXTEND Gram
ssr_elsepat: [[ "else" -> { [[CAst.make ~loc @@ CPatAtom None]] } ]];
ssr_else: [[ mp = ssr_elsepat; c = lconstr -> { CAst.make ~loc (mp, c) } ]];
binder_constr: [
- [ "if"; c = operconstr LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else ->
+ [ "if"; c = term LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else ->
{ let b1, ct, rt = db1 in CAst.make ~loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) }
- | "if"; c = operconstr LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else ->
+ | "if"; c = term LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else ->
{ let b1, ct, rt = db1 in
let b1, b2 = let open CAst in
let {loc=l1; v=(p1, r1)}, {loc=l2; v=(p2, r2)} = b1, b2 in
@@ -119,7 +119,7 @@ END
GRAMMAR EXTEND Gram
GLOBAL: closed_binder;
closed_binder: [
- [ ["of" -> { () } | "&" -> { () } ]; c = operconstr LEVEL "99" ->
+ [ ["of" -> { () } | "&" -> { () } ]; c = term LEVEL "99" ->
{ [CLocalAssum ([CAst.make ~loc Anonymous], Default Explicit, c)] }
] ];
END
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 16:08:29 +0000