aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrast.mli2
-rw-r--r--plugins/ssr/ssrcommon.ml11
-rw-r--r--plugins/ssr/ssrelim.ml2
-rw-r--r--plugins/ssr/ssrfwd.ml1
-rw-r--r--plugins/ssr/ssrparser.ml440
-rw-r--r--plugins/ssr/ssrtacticals.ml3
-rw-r--r--plugins/ssr/ssrtacticals.mli4
-rw-r--r--plugins/ssr/ssrvernac.ml417
-rw-r--r--plugins/ssr/ssrview.ml2
9 files changed, 39 insertions, 43 deletions
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index 7f5f2f63d..5571c5420 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -37,7 +37,7 @@ type ssrmult = int * ssrmmod
type ssrocc = (bool * int list) option
(* index MAYBE REMOVE ONLY INTERNAL stuff between {} *)
-type ssrindex = int Misctypes.or_var
+type ssrindex = int Locus.or_var
(* clear switch {H G} *)
type ssrclear = ssrhyps
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 3f6503e73..54f3f9c71 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -181,10 +181,9 @@ let option_assert_get o msg =
(** Constructors for rawconstr *)
open Glob_term
open Globnames
-open Misctypes
open Decl_kinds
-let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None)
+let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None)
let rec mkRHoles n = if n > 0 then mkRHole :: mkRHoles (n - 1) else []
let rec isRHoles cl = match cl with
@@ -254,7 +253,7 @@ let interp_refine ist gl rc =
let interp_open_constr ist gl gc =
- let (sigma, (c, _)) = Tacinterp.interp_open_constr_with_bindings ist (pf_env gl) (project gl) (gc, Misctypes.NoBindings) in
+ let (sigma, (c, _)) = Tacinterp.interp_open_constr_with_bindings ist (pf_env gl) (project gl) (gc, Tactypes.NoBindings) in
(project gl, (sigma, c))
let interp_term ist gl (_, c) = snd (interp_open_constr ist gl c)
@@ -859,10 +858,10 @@ open Util
(** Constructors for constr_expr *)
let mkCProp loc = CAst.make ?loc @@ CSort GProp
let mkCType loc = CAst.make ?loc @@ CSort (GType [])
-let mkCVar ?loc id = CAst.make ?loc @@ CRef (CAst.make ?loc @@ Ident id, None)
+let mkCVar ?loc id = CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None)
let rec mkCHoles ?loc n =
- if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) :: mkCHoles ?loc (n - 1)
-let mkCHole loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None)
+ if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None)) :: mkCHoles ?loc (n - 1)
+let mkCHole loc = CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None)
let mkCLambda ?loc name ty t = CAst.make ?loc @@
CLambdaN ([CLocalAssum([CAst.make ?loc name], Default Explicit, ty)], t)
let mkCArrow ?loc ty t = CAst.make ?loc @@
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 83b4d6562..fbe3b000f 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -17,7 +17,7 @@ open Term
open Constr
open Termops
open Globnames
-open Misctypes
+open Tactypes
open Tacmach
open Ssrmatching_plugin
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index c6beb08c5..2c046190f 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -86,7 +86,6 @@ let _ =
open Constrexpr
open Glob_term
-open Misctypes
let combineCG t1 t2 f g = match t1, t2 with
| (x, (t1, None)), (_, (t2, None)) -> x, (g t1 t2, None)
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index fbfbdb110..7a1d06fdc 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -22,13 +22,15 @@ open Libnames
open Tactics
open Tacmach
open Util
+open Locus
open Tacexpr
open Tacinterp
open Pltac
open Extraargs
open Ppconstr
-open Misctypes
+open Namegen
+open Tactypes
open Decl_kinds
open Constrexpr
open Constrexpr_ops
@@ -301,24 +303,24 @@ END
let pr_index = function
- | Misctypes.ArgVar {CAst.v=id} -> pr_id id
- | Misctypes.ArgArg n when n > 0 -> int n
+ | ArgVar {CAst.v=id} -> pr_id id
+ | ArgArg n when n > 0 -> int n
| _ -> mt ()
let pr_ssrindex _ _ _ = pr_index
-let noindex = Misctypes.ArgArg 0
+let noindex = ArgArg 0
let check_index ?loc i =
if i > 0 then i else CErrors.user_err ?loc (str"Index not positive")
let mk_index ?loc = function
- | Misctypes.ArgArg i -> Misctypes.ArgArg (check_index ?loc i)
+ | ArgArg i -> ArgArg (check_index ?loc i)
| iv -> iv
let interp_index ist gl idx =
Tacmach.project gl,
match idx with
- | Misctypes.ArgArg _ -> idx
- | Misctypes.ArgVar id ->
+ | ArgArg _ -> idx
+ | ArgVar id ->
let i =
try
let v = Id.Map.find id.CAst.v ist.Tacinterp.lfun in
@@ -336,7 +338,7 @@ let interp_index ist gl idx =
| None -> raise Not_found
end end
with _ -> CErrors.user_err ?loc:id.CAst.loc (str"Index not a number") in
- Misctypes.ArgArg (check_index ?loc:id.CAst.loc i)
+ ArgArg (check_index ?loc:id.CAst.loc i)
open Pltac
@@ -543,7 +545,7 @@ END
let remove_loc x = x.CAst.v
-let ipat_of_intro_pattern p = Misctypes.(
+let ipat_of_intro_pattern p = Tactypes.(
let rec ipat_of_intro_pattern = function
| IntroNaming (IntroIdentifier id) -> IPatId id
| IntroAction IntroWildcard -> IPatAnon Drop
@@ -595,16 +597,15 @@ let intern_ipats ist = List.map (intern_ipat ist)
let interp_intro_pattern = interp_wit wit_intro_pattern
-let interp_introid ist gl id = Misctypes.(
+let interp_introid ist gl id =
try IntroNaming (IntroIdentifier (hyp_id (snd (interp_hyp ist gl (SsrHyp (Loc.tag id))))))
with _ -> (snd (interp_intro_pattern ist gl (CAst.make @@ IntroNaming (IntroIdentifier id)))).CAst.v
-)
let get_intro_id = function
| IntroNaming (IntroIdentifier id) -> id
| _ -> assert false
-let rec add_intro_pattern_hyps ipat hyps = Misctypes.(
+let rec add_intro_pattern_hyps ipat hyps =
let {CAst.loc=loc;v=ipat} = ipat in
match ipat with
| IntroNaming (IntroIdentifier id) ->
@@ -623,7 +624,6 @@ let rec add_intro_pattern_hyps ipat hyps = Misctypes.(
| IntroForthcoming _ ->
(* As in ipat_of_intro_pattern, was unable to determine which kind
of ipat interp_introid could return [HH] *) assert false
-)
(* We interp the ipat using the standard ltac machinery for ids, since
* we have no clue what a name could be bound to (maybe another ipat) *)
@@ -1064,7 +1064,7 @@ let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with
| BFdef :: h, { v = CLetIn({CAst.v=x}, v, oty, c) } ->
let bs, c' = format_constr_expr h c in
Bdef (x, oty, v) :: bs, c'
- | [BFcast], { v = CCast (c, CastConv t) } ->
+ | [BFcast], { v = CCast (c, Glob_term.CastConv t) } ->
[Bcast t], c
| BFrec (has_str, has_cast) :: h,
{ v = CFix ( _, [_, (Some locn, CStructRec), bl, t, c]) } ->
@@ -1093,7 +1093,7 @@ let wit_ssrfwdfmt = add_genarg "ssrfwdfmt" pr_fwdfmt
let mkFwdVal fk c = ((fk, []), c)
let mkssrFwdVal fk c = ((fk, []), (c,None))
-let dC t = CastConv t
+let dC t = Glob_term.CastConv t
let same_ist { interp_env = x } { interp_env = y } =
match x,y with
@@ -1154,7 +1154,8 @@ ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY pr_ssrbvar
END
let bvar_lname = let open CAst in function
- | { v = CRef ({loc;v=Ident id}, _) } -> CAst.make ?loc @@ Name id
+ | { v = CRef (qid, _) } when qualid_is_ident qid ->
+ CAst.make ?loc:qid.CAst.loc @@ Name (qualid_basename qid)
| { loc = loc } -> CAst.make ?loc Anonymous
let pr_ssrbinder prc _ _ (_, c) = prc c
@@ -1210,8 +1211,8 @@ let push_binders c2 bs =
| [] -> c
| _ -> anomaly "binder not a lambda nor a let in" in
match c2 with
- | { loc; v = CCast (ct, CastConv cty) } ->
- CAst.make ?loc @@ (CCast (loop false ct bs, CastConv (loop true cty bs)))
+ | { loc; v = CCast (ct, Glob_term.CastConv cty) } ->
+ CAst.make ?loc @@ (CCast (loop false ct bs, Glob_term.CastConv (loop true cty bs)))
| ct -> loop false ct bs
let rec fix_binders = let open CAst in function
@@ -1246,7 +1247,8 @@ END
let pr_ssrfixfwd _ _ _ (id, fwd) = str " fix " ++ pr_id id ++ pr_fwd fwd
let bvar_locid = function
- | { CAst.v = CRef ({CAst.loc=loc;v=Ident id}, _) } -> CAst.make ?loc id
+ | { CAst.v = CRef (qid, _) } when qualid_is_ident qid ->
+ CAst.make ?loc:qid.CAst.loc (qualid_basename qid)
| _ -> CErrors.user_err (Pp.str "Missing identifier after \"(co)fix\"")
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index 372ae86bd..83581f341 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -14,7 +14,6 @@ open Names
open Constr
open Termops
open Tacmach
-open Misctypes
open Locusops
open Ssrast
@@ -25,7 +24,7 @@ module NamedDecl = Context.Named.Declaration
(** Tacticals (+, -, *, done, by, do, =>, first, and last). *)
-let get_index = function ArgArg i -> i | _ ->
+let get_index = function Locus.ArgArg i -> i | _ ->
anomaly "Uninterpreted index"
(* Toplevel constr must be globalized twice ! *)
diff --git a/plugins/ssr/ssrtacticals.mli b/plugins/ssr/ssrtacticals.mli
index a5636ad0f..684e00235 100644
--- a/plugins/ssr/ssrtacticals.mli
+++ b/plugins/ssr/ssrtacticals.mli
@@ -17,7 +17,7 @@ val tclSEQAT :
Tacinterp.interp_sign ->
Tacinterp.Value.t ->
Ssrast.ssrdir ->
- int Misctypes.or_var *
+ int Locus.or_var *
(('a * Tacinterp.Value.t option list) *
Tacinterp.Value.t option) ->
Tacmach.tactic
@@ -37,7 +37,7 @@ val hinttac :
val ssrdotac :
Tacinterp.interp_sign ->
- ((int Misctypes.or_var * Ssrast.ssrmmod) *
+ ((int Locus.or_var * Ssrast.ssrmmod) *
(bool * Tacinterp.Value.t option list)) *
((Ssrast.ssrhyps *
((Ssrast.ssrhyp_or_id * string) *
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 750461a1b..7ce2dd64a 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -27,9 +27,7 @@ open Glob_term
open Globnames
open Stdarg
open Genarg
-open Misctypes
open Decl_kinds
-open Libnames
open Pp
open Ppconstr
open Printer
@@ -144,21 +142,21 @@ END
let declare_one_prenex_implicit locality f =
let fref =
try Smartlocate.global_with_alias f
- with _ -> errorstrm (pr_reference f ++ str " is not declared") in
+ with _ -> errorstrm (pr_qualid f ++ str " is not declared") in
let rec loop = function
| a :: args' when Impargs.is_status_implicit a ->
(ExplByName (Impargs.name_of_implicit a), (true, true, true)) :: loop args'
| args' when List.exists Impargs.is_status_implicit args' ->
- errorstrm (str "Expected prenex implicits for " ++ pr_reference f)
+ errorstrm (str "Expected prenex implicits for " ++ pr_qualid f)
| _ -> [] in
let impls =
match Impargs.implicits_of_global fref with
| [cond,impls] -> impls
- | [] -> errorstrm (str "Expected some implicits for " ++ pr_reference f)
+ | [] -> errorstrm (str "Expected some implicits for " ++ pr_qualid f)
| _ -> errorstrm (str "Multiple implicits not supported") in
match loop impls with
| [] ->
- errorstrm (str "Expected some implicits for " ++ pr_reference f)
+ errorstrm (str "Expected some implicits for " ++ pr_qualid f)
| impls ->
Impargs.declare_manual_implicits locality fref ~enriching:false [impls]
@@ -416,7 +414,7 @@ let interp_search_arg arg =
(* Module path postfilter *)
-let pr_modloc (b, m) = if b then str "-" ++ pr_reference m else pr_reference m
+let pr_modloc (b, m) = if b then str "-" ++ pr_qualid m else pr_qualid m
let wit_ssrmodloc = add_genarg "ssrmodloc" pr_modloc
@@ -434,10 +432,9 @@ GEXTEND Gram
END
let interp_modloc mr =
- let interp_mod (_, mr) =
- let {CAst.loc=loc; v=qid} = qualid_of_reference mr in
+ let interp_mod (_, qid) =
try Nametab.full_name_module qid with Not_found ->
- CErrors.user_err ?loc (str "No Module " ++ pr_qualid qid) in
+ CErrors.user_err ?loc:qid.CAst.loc (str "No Module " ++ pr_qualid qid) in
let mr_out, mr_in = List.partition fst mr in
let interp_bmod b = function
| [] -> fun _ _ _ -> true
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 29a936381..faebe3179 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -157,7 +157,7 @@ let tclINJ_CONSTR_IST ist p =
let mkGHole =
DAst.make
- (Glob_term.GHole(Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None))
+ (Glob_term.GHole(Evar_kinds.InternalHole, Namegen.IntroAnonymous, None))
let rec mkGHoles n = if n > 0 then mkGHole :: mkGHoles (n - 1) else []
let mkGApp f args =
if args = [] then f
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-25 18:01:45 +0000