aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrast.mli1
-rw-r--r--plugins/ssr/ssrbwd.ml1
-rw-r--r--plugins/ssr/ssrbwd.mli1
-rw-r--r--plugins/ssr/ssrcommon.ml2
-rw-r--r--plugins/ssr/ssrcommon.mli3
-rw-r--r--plugins/ssr/ssrelim.ml1
-rw-r--r--plugins/ssr/ssrelim.mli1
-rw-r--r--plugins/ssr/ssrequality.ml1
-rw-r--r--plugins/ssr/ssrequality.mli1
-rw-r--r--plugins/ssr/ssrfwd.ml1
-rw-r--r--plugins/ssr/ssrfwd.mli1
-rw-r--r--plugins/ssr/ssripats.ml1
-rw-r--r--plugins/ssr/ssripats.mli1
-rw-r--r--plugins/ssr/ssrparser.ml42
-rw-r--r--plugins/ssr/ssrparser.mli5
-rw-r--r--plugins/ssr/ssrprinters.ml1
-rw-r--r--plugins/ssr/ssrprinters.mli27
-rw-r--r--plugins/ssr/ssrtacticals.ml1
-rw-r--r--plugins/ssr/ssrtacticals.mli1
-rw-r--r--plugins/ssr/ssrvernac.ml45
-rw-r--r--plugins/ssr/ssrview.ml1
-rw-r--r--plugins/ssr/ssrview.mli1
22 files changed, 17 insertions, 43 deletions
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index 94eaa1d6aa..cdd4ee6459 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Names
open Ltac_plugin
diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml
index 3988f00bad..cc0e86684e 100644
--- a/plugins/ssr/ssrbwd.ml
+++ b/plugins/ssr/ssrbwd.ml
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Printer
open Pretyping
open Globnames
diff --git a/plugins/ssr/ssrbwd.mli b/plugins/ssr/ssrbwd.mli
index 20a1263d24..af9f7491ad 100644
--- a/plugins/ssr/ssrbwd.mli
+++ b/plugins/ssr/ssrbwd.mli
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
val apply_top_tac : Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 411ce6853c..799e969ae2 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -8,8 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
-open Grammar_API
open Util
open Names
open Evd
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index f611685769..2eadd5f26c 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Tacmach
open Names
open Environ
@@ -42,7 +41,7 @@ val nohint : 'a ssrhint
(******************************** misc ************************************)
-val errorstrm : Pp.std_ppcmds -> 'a
+val errorstrm : Pp.t -> 'a
val anomaly : string -> 'a
val array_app_tl : 'a array -> 'a list -> 'a list
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index bd9a05891a..832044909c 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Util
open Names
open Printer
diff --git a/plugins/ssr/ssrelim.mli b/plugins/ssr/ssrelim.mli
index 825b4758e3..66e202b48f 100644
--- a/plugins/ssr/ssrelim.mli
+++ b/plugins/ssr/ssrelim.mli
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Ssrmatching_plugin
val ssrelim :
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index b0fe898975..ab6a60f4ee 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Ltac_plugin
open Util
open Names
diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli
index f9ab5d74fe..a3366887fb 100644
--- a/plugins/ssr/ssrequality.mli
+++ b/plugins/ssr/ssrequality.mli
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Ssrmatching_plugin
open Ssrast
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 660c2e776c..8e6329a15e 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Names
open Tacmach
diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli
index 7f254074c7..e5b5b58fff 100644
--- a/plugins/ssr/ssrfwd.mli
+++ b/plugins/ssr/ssrfwd.mli
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Names
open Ltac_plugin
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 06bbd749e6..023778fdbf 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Names
open Pp
open Term
diff --git a/plugins/ssr/ssripats.mli b/plugins/ssr/ssripats.mli
index aefdc8e111..6c36e67e83 100644
--- a/plugins/ssr/ssripats.mli
+++ b/plugins/ssr/ssripats.mli
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Ssrmatching_plugin
open Ssrast
open Ssrcommon
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 09917339a7..ce23bb2b30 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -8,8 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
-open Grammar_API
open Names
open Pp
open Pcoq
diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index 1548206666..88beeaa711 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -8,9 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
-open Grammar_API
-
val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
val pr_ssrtacarg : 'a -> 'b -> (int * Ppextend.parenRelation -> 'c) -> 'c
@@ -19,5 +16,5 @@ val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
val pr_ssrtclarg : 'a -> 'b -> (int * Ppextend.parenRelation -> 'c -> 'd) -> 'c -> 'd
-val add_genarg : string -> ('a -> Pp.std_ppcmds) -> 'a Genarg.uniform_genarg_type
+val add_genarg : string -> ('a -> Pp.t) -> 'a Genarg.uniform_genarg_type
diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml
index 427109c1b2..e865ef706d 100644
--- a/plugins/ssr/ssrprinters.ml
+++ b/plugins/ssr/ssrprinters.ml
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Pp
open Names
open Printer
diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli
index 8da9bc72bc..f231068265 100644
--- a/plugins/ssr/ssrprinters.mli
+++ b/plugins/ssr/ssrprinters.mli
@@ -8,20 +8,19 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Ssrast
val pp_term :
- Goal.goal Evd.sigma -> EConstr.constr -> Pp.std_ppcmds
+ Goal.goal Evd.sigma -> EConstr.constr -> Pp.t
-val pr_spc : unit -> Pp.std_ppcmds
-val pr_bar : unit -> Pp.std_ppcmds
+val pr_spc : unit -> Pp.t
+val pr_bar : unit -> Pp.t
val pr_list :
- (unit -> Pp.std_ppcmds) -> ('a -> Pp.std_ppcmds) -> 'a list -> Pp.std_ppcmds
+ (unit -> Pp.t) -> ('a -> Pp.t) -> 'a list -> Pp.t
val pp_concat :
- Pp.std_ppcmds ->
- ?sep:Pp.std_ppcmds -> Pp.std_ppcmds list -> Pp.std_ppcmds
+ Pp.t ->
+ ?sep:Pp.t -> Pp.t list -> Pp.t
val xInParens : ssrtermkind
val xWithAt : ssrtermkind
@@ -30,17 +29,17 @@ val xCpattern : ssrtermkind
val pr_term :
ssrtermkind * (Glob_term.glob_constr * Constrexpr.constr_expr option) ->
- Pp.std_ppcmds
+ Pp.t
-val pr_hyp : ssrhyp -> Pp.std_ppcmds
+val pr_hyp : ssrhyp -> Pp.t
-val prl_constr_expr : Constrexpr.constr_expr -> Pp.std_ppcmds
-val prl_glob_constr : Glob_term.glob_constr -> Pp.std_ppcmds
+val prl_constr_expr : Constrexpr.constr_expr -> Pp.t
+val prl_glob_constr : Glob_term.glob_constr -> Pp.t
val pr_guarded :
- (string -> int -> bool) -> ('a -> Pp.std_ppcmds) -> 'a -> Pp.std_ppcmds
+ (string -> int -> bool) -> ('a -> Pp.t) -> 'a -> Pp.t
-val pr_occ : ssrocc -> Pp.std_ppcmds
+val pr_occ : ssrocc -> Pp.t
-val ppdebug : Pp.std_ppcmds Lazy.t -> unit
+val ppdebug : Pp.t Lazy.t -> unit
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index b586d05e1c..5e43c83749 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Names
open Termops
open Tacmach
diff --git a/plugins/ssr/ssrtacticals.mli b/plugins/ssr/ssrtacticals.mli
index 297cfdfdc0..c1f65a31e9 100644
--- a/plugins/ssr/ssrtacticals.mli
+++ b/plugins/ssr/ssrtacticals.mli
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
val tclSEQAT :
Ltac_plugin.Tacinterp.interp_sign ->
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 4c8827bf84..9c59d83d4e 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -8,8 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
-open Grammar_API
open Names
open Term
open Termops
@@ -337,7 +335,8 @@ let coerce_search_pattern_to_sort hpat =
Pattern.PApp (fp, args') in
let hr, na = splay_search_pattern 0 hpat in
let dc, ht =
- Reductionops.splay_prod env sigma (EConstr.of_constr (Universes.unsafe_type_of_global hr)) in
+ let hr, _ = Global.type_of_global_in_context (Global.env ()) hr (** FIXME *) in
+ Reductionops.splay_prod env sigma (EConstr.of_constr hr) in
let np = List.length dc in
if np < na then CErrors.user_err (Pp.str "too many arguments in head search pattern") else
let hpat' = if np = na then hpat else mkPApp hpat (np - na) [||] in
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index cc142e091c..338ecccc2d 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Util
open Names
open Term
diff --git a/plugins/ssr/ssrview.mli b/plugins/ssr/ssrview.mli
index 8a7bd5d6e7..6fd906ff4f 100644
--- a/plugins/ssr/ssrview.mli
+++ b/plugins/ssr/ssrview.mli
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Ssrast
open Ssrcommon
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 19:47:37 +0000