aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/funind/gen_principle.ml2
-rw-r--r--plugins/funind/glob_term_to_relation.ml2
-rw-r--r--plugins/funind/glob_termops.ml1
-rw-r--r--plugins/ltac/g_tactic.mlg5
-rw-r--r--plugins/ltac/pptactic.ml3
-rw-r--r--plugins/ssr/ssrcommon.ml1
-rw-r--r--plugins/ssr/ssrparser.mlg15
-rw-r--r--plugins/ssr/ssrvernac.mlg1
-rw-r--r--plugins/ssrmatching/ssrmatching.ml1
-rw-r--r--plugins/syntax/numeral.ml2
-rw-r--r--plugins/syntax/string_notation.ml2
11 files changed, 14 insertions, 21 deletions
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 730ae48393..a836335d4d 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -1600,7 +1600,7 @@ let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt w
let b = Names.Id.of_string "___b" in
Constrexpr_ops.mkLambdaC(
[CAst.make @@ Name a; CAst.make @@ Name b],
- Constrexpr.Default Decl_kinds.Explicit,
+ Constrexpr.Default Glob_term.Explicit,
wf_arg_type,
Constrexpr_ops.mkAppC(wf_rel_expr,
[
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 6eb8c42d1d..ddd6ecfb5c 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1300,7 +1300,7 @@ let rec rebuild_return_type rt =
| Constrexpr.CLetIn(na,v,t,t') ->
CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t')
| _ -> CAst.make ?loc @@ Constrexpr.CProdN([Constrexpr.CLocalAssum ([CAst.make Anonymous],
- Constrexpr.Default Decl_kinds.Explicit, rt)],
+ Constrexpr.Default Explicit, rt)],
CAst.make @@ Constrexpr.CSort(UAnonymous {rigid=true}))
let do_build_inductive
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index d36d86a65b..fbf63c69dd 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -4,7 +4,6 @@ open Glob_term
open CErrors
open Util
open Names
-open Decl_kinds
(*
Some basic functions to rebuild glob_constr
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 7cd43cb5cd..9b52b710c1 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -24,7 +24,6 @@ open Tactypes
open Tactics
open Inv
open Locus
-open Decl_kinds
open Pcoq
@@ -450,9 +449,9 @@ GRAMMAR EXTEND Gram
| -> { true } ] ]
;
simple_binder:
- [ [ na=name -> { ([na],Default Explicit, CAst.make ~loc @@
+ [ [ na=name -> { ([na],Default Glob_term.Explicit, CAst.make ~loc @@
CHole (Some (Evar_kinds.BinderType na.CAst.v), IntroAnonymous, None)) }
- | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> { (nal,Default Explicit,c) }
+ | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> { (nal,Default Glob_term.Explicit,c) }
] ]
;
fixdecl:
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 0e38ce575b..6df068883c 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -20,7 +20,6 @@ open Stdarg
open Notation_gram
open Tactypes
open Locus
-open Decl_kinds
open Genredexpr
open Ppconstr
open Pputils
@@ -1097,7 +1096,7 @@ let pr_goal_selector ~toplevel s =
let rec strip_ty acc n ty =
if Int.equal n 0 then (List.rev acc, (ty,None)) else
match DAst.get ty with
- Glob_term.GProd(na,Explicit,a,b) ->
+ Glob_term.GProd(na,Glob_term.Explicit,a,b) ->
strip_ty (([CAst.make na],(a,None))::acc) (n-1) b
| _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
strip_ty [] n ty
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 33e9f871fd..473612fda7 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -181,7 +181,6 @@ let option_assert_get o msg =
(** Constructors for rawconstr *)
open Glob_term
-open Decl_kinds
let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None)
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 175a863ad8..a1f707ffa8 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -32,7 +32,6 @@ open Ppconstr
open Namegen
open Tactypes
-open Decl_kinds
open Constrexpr
open Constrexpr_ops
@@ -1337,20 +1336,20 @@ ARGUMENT EXTEND ssrbinder TYPED AS (ssrfwdfmt * constr) PRINTED BY { pr_ssrbinde
| [ ssrbvar(bv) ] ->
{ let { CAst.loc=xloc } as x = bvar_lname bv in
(FwdPose, [BFvar]),
- CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) }
+ CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Glob_term.Explicit,mkCHole xloc)],mkCHole (Some loc)) }
| [ "(" ssrbvar(bv) ")" ] ->
{ let { CAst.loc=xloc } as x = bvar_lname bv in
(FwdPose, [BFvar]),
- CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) }
+ CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Glob_term.Explicit,mkCHole xloc)],mkCHole (Some loc)) }
| [ "(" ssrbvar(bv) ":" lconstr(t) ")" ] ->
{ let x = bvar_lname bv in
(FwdPose, [BFdecl 1]),
- CAst.make ~loc @@ CLambdaN ([CLocalAssum([x], Default Explicit, t)], mkCHole (Some loc)) }
+ CAst.make ~loc @@ CLambdaN ([CLocalAssum([x], Default Glob_term.Explicit, t)], mkCHole (Some loc)) }
| [ "(" ssrbvar(bv) ne_ssrbvar_list(bvs) ":" lconstr(t) ")" ] ->
{ let xs = List.map bvar_lname (bv :: bvs) in
let n = List.length xs in
(FwdPose, [BFdecl n]),
- CAst.make ~loc @@ CLambdaN ([CLocalAssum (xs, Default Explicit, t)], mkCHole (Some loc)) }
+ CAst.make ~loc @@ CLambdaN ([CLocalAssum (xs, Default Glob_term.Explicit, t)], mkCHole (Some loc)) }
| [ "(" ssrbvar(id) ":" lconstr(t) ":=" lconstr(v) ")" ] ->
{ (FwdPose,[BFdef]), CAst.make ~loc @@ CLetIn (bvar_lname id, v, Some t, mkCHole (Some loc)) }
| [ "(" ssrbvar(id) ":=" lconstr(v) ")" ] ->
@@ -1362,7 +1361,7 @@ GRAMMAR EXTEND Gram
ssrbinder: [
[ ["of" -> { () } | "&" -> { () } ]; c = operconstr LEVEL "99" -> {
(FwdPose, [BFvar]),
- CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Explicit,c)],mkCHole (Some loc)) } ]
+ CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Glob_term.Explicit,c)],mkCHole (Some loc)) } ]
];
END
@@ -1391,7 +1390,7 @@ let push_binders c2 bs =
let rec fix_binders = let open CAst in function
| (_, { v = CLambdaN ([CLocalAssum(xs, _, t)], _) } ) :: bs ->
- CLocalAssum (xs, Default Explicit, t) :: fix_binders bs
+ CLocalAssum (xs, Default Glob_term.Explicit, t) :: fix_binders bs
| (_, { v = CLetIn (x, v, oty, _) } ) :: bs ->
CLocalDef (x, v, oty) :: fix_binders bs
| _ -> []
@@ -1521,7 +1520,7 @@ let intro_id_to_binder = List.map (function
| IPatId id ->
let { CAst.loc=xloc } as x = bvar_lname (mkCVar id) in
(FwdPose, [BFvar]),
- CAst.make @@ CLambdaN ([CLocalAssum([x], Default Explicit, mkCHole xloc)],
+ CAst.make @@ CLambdaN ([CLocalAssum([x], Default Glob_term.Explicit, mkCHole xloc)],
mkCHole None)
| _ -> anomaly "non-id accepted as binder")
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 0adabb0673..f3f1d713e9 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -27,7 +27,6 @@ open Notation_ops
open Notation_term
open Glob_term
open Stdarg
-open Decl_kinds
open Pp
open Ppconstr
open Printer
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 17db25660f..4d7a04f5ee 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -36,7 +36,6 @@ open Ppconstr
open Printer
open Globnames
open Namegen
-open Decl_kinds
open Evar_kinds
open Constrexpr
open Constrexpr_ops
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index a148a3bc73..9808c61255 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -112,7 +112,7 @@ let vernac_numeral_notation local ty f g scope opts =
let cty = mkRefC ty in
let app x y = mkAppC (x,[y]) in
let arrow x y =
- mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y)
+ mkProdC ([CAst.make Anonymous],Default Glob_term.Explicit, x, y)
in
let opt r = app (mkRefC (q_option ())) r in
let constructors = get_constructors tyc in
diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml
index 8c0f9a3339..c92acb0f55 100644
--- a/plugins/syntax/string_notation.ml
+++ b/plugins/syntax/string_notation.ml
@@ -61,7 +61,7 @@ let vernac_string_notation local ty f g scope =
let of_ty = Smartlocate.global_with_alias g in
let cty = cref ty in
let arrow x y =
- mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y)
+ mkProdC ([CAst.make Anonymous],Default Glob_term.Explicit, x, y)
in
let constructors = get_constructors tyc in
(* Check the type of f *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:13:07 +0000