aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/mlutil.ml3
-rw-r--r--plugins/funind/functional_principles_proofs.ml4
-rw-r--r--plugins/funind/gen_principle.ml27
-rw-r--r--plugins/funind/glob_termops.ml2
-rw-r--r--plugins/funind/indfun.ml6
-rw-r--r--plugins/ltac/g_tactic.mlg14
-rw-r--r--plugins/ssr/ssrparser.mlg70
-rw-r--r--plugins/ssrmatching/g_ssrmatching.mlg4
8 files changed, 65 insertions, 65 deletions
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index cfdaac710b..268d4bf9e9 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1525,8 +1525,7 @@ let inline_test r t =
else
let c = match r with GlobRef.ConstRef c -> c | _ -> assert false in
let has_body =
- try constant_has_body (Global.lookup_constant c)
- with Not_found -> false
+ Environ.mem_constant c (Global.env()) && constant_has_body (Global.lookup_constant c)
in
has_body &&
(let t1 = eta_red t in
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 3234d40f73..7d19c443e9 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -930,8 +930,8 @@ let do_replace (evd : Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num
(* let res = Constrintern.construct_reference (pf_hyps g) equation_lemma_id in *)
let evd', res =
Evd.fresh_global (Global.env ()) !evd
- (Constrintern.locate_reference
- (qualid_of_ident equation_lemma_id))
+ (Option.get (Constrintern.locate_reference
+ (qualid_of_ident equation_lemma_id)))
in
evd := evd';
let sigma, _ =
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index cbdebb7bbc..f1a3cb6af8 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -241,7 +241,7 @@ let change_property_sort evd toSort princ princName =
in
let evd, princName_as_constr =
Evd.fresh_global (Global.env ()) evd
- (Constrintern.locate_reference (Libnames.qualid_of_ident princName))
+ (Option.get (Constrintern.locate_reference (Libnames.qualid_of_ident princName)))
in
let init =
let nargs =
@@ -408,8 +408,8 @@ let register_struct is_rec fixpoint_exprl =
(fun (evd, l) {Vernacexpr.fname} ->
let evd, c =
Evd.fresh_global (Global.env ()) evd
- (Constrintern.locate_reference
- (Libnames.qualid_of_ident fname.CAst.v))
+ (Option.get (Constrintern.locate_reference
+ (Libnames.qualid_of_ident fname.CAst.v)))
in
let cst, u = destConst evd c in
let u = EInstance.kind evd u in
@@ -427,8 +427,8 @@ let register_struct is_rec fixpoint_exprl =
(fun (evd, l) {Vernacexpr.fname} ->
let evd, c =
Evd.fresh_global (Global.env ()) evd
- (Constrintern.locate_reference
- (Libnames.qualid_of_ident fname.CAst.v))
+ (Option.get (Constrintern.locate_reference
+ (Libnames.qualid_of_ident fname.CAst.v)))
in
let cst, u = destConst evd c in
let u = EInstance.kind evd u in
@@ -1522,7 +1522,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
(* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *)
let _, lem_cst_constr =
Evd.fresh_global (Global.env ()) !evd
- (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id))
+ (Option.get (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)))
in
let lem_cst, _ = EConstr.destConst !evd lem_cst_constr in
update_Function {finfo with correctness_lemma = Some lem_cst})
@@ -1592,7 +1592,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
in
let _, lem_cst_constr =
Evd.fresh_global (Global.env ()) !evd
- (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id))
+ (Option.get (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)))
in
let lem_cst, _ = destConst !evd lem_cst_constr in
update_Function {finfo with completeness_lemma = Some lem_cst})
@@ -1615,7 +1615,7 @@ let derive_inversion fix_names =
(fun id (evd, l) ->
let evd, c =
Evd.fresh_global (Global.env ()) evd
- (Constrintern.locate_reference (Libnames.qualid_of_ident id))
+ (Option.get (Constrintern.locate_reference (Libnames.qualid_of_ident id)))
in
let cst, u = EConstr.destConst evd c in
(evd, (cst, EConstr.EInstance.kind evd u) :: l))
@@ -1635,8 +1635,8 @@ let derive_inversion fix_names =
(fun id (evd, l) ->
let evd, id =
Evd.fresh_global (Global.env ()) evd
- (Constrintern.locate_reference
- (Libnames.qualid_of_ident (mk_rel_id id)))
+ (Option.get (Constrintern.locate_reference
+ (Libnames.qualid_of_ident (mk_rel_id id))))
in
(evd, fst (EConstr.destInd evd id) :: l))
fix_names (evd', [])
@@ -2058,13 +2058,12 @@ let make_graph (f_ref : GlobRef.t) =
let sigma = Evd.from_env env in
let c, c_body =
match f_ref with
- | GlobRef.ConstRef c -> (
- try (c, Global.lookup_constant c)
- with Not_found ->
+ | GlobRef.ConstRef c ->
+ if Environ.mem_constant c (Global.env ()) then (c, Global.lookup_constant c) else
CErrors.user_err
Pp.(
str "Cannot find "
- ++ Printer.pr_leconstr_env env sigma (EConstr.mkConst c)) )
+ ++ Printer.pr_leconstr_env env sigma (EConstr.mkConst c))
| _ -> CErrors.user_err Pp.(str "Not a function reference")
in
match Global.body_of_constant_body Library.indirect_accessor c_body with
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 164a446fe3..fb00d2f202 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -342,7 +342,7 @@ let is_free_in id =
| GRec _ -> user_err Pp.(str "Not handled GRec") | GSort _ -> false
| GHole _ -> false
| GCast (b, (CastConv t | CastVM t | CastNative t)) ->
- is_free_in b || is_free_in t | GCast (b, CastCoerce) -> is_free_in b
+ is_free_in b || is_free_in t
| GInt _ | GFloat _ -> false
| GArray (_u, t, def, ty) ->
Array.exists is_free_in t || is_free_in def || is_free_in ty)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 4e0e2dc501..1221ad0bda 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -80,10 +80,12 @@ let functional_induction with_clean c princl pat =
(elimination_sort_of_goal gl)
in
let princ_ref =
- try
+ match
Constrintern.locate_reference
(Libnames.qualid_of_ident princ_name)
- with Not_found ->
+ with
+ | Some r -> r
+ | None ->
user_err
( str "Cannot find induction principle for "
++ Printer.pr_leconstr_env (pf_env gl) sigma (mkConst c') )
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index cb430efb40..9dec55e020 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -59,28 +59,28 @@ open Extraargs
(* idem for (x1..xn:t) [n^2 complexity but exceptional use] *)
let check_for_coloneq =
- Pcoq.Entry.of_parser "lpar_id_colon"
- (fun _ strm ->
+ Pcoq.Entry.(of_parser "lpar_id_colon"
+ { parser_fun = fun strm ->
let rec skip_to_rpar p n =
- match List.last (Stream.npeek n strm) with
+ match List.last (LStream.npeek n strm) with
| KEYWORD "(" -> skip_to_rpar (p+1) (n+1)
| KEYWORD ")" -> if Int.equal p 0 then n+1 else skip_to_rpar (p-1) (n+1)
| KEYWORD "." -> err ()
| _ -> skip_to_rpar p (n+1) in
let rec skip_names n =
- match List.last (Stream.npeek n strm) with
+ match List.last (LStream.npeek n strm) with
| IDENT _ | KEYWORD "_" -> skip_names (n+1)
| KEYWORD ":" -> skip_to_rpar 0 (n+1) (* skip a constr *)
| _ -> err () in
let rec skip_binders n =
- match List.last (Stream.npeek n strm) with
+ match List.last (LStream.npeek n strm) with
| KEYWORD "(" -> skip_binders (skip_names (n+1))
| IDENT _ | KEYWORD "_" -> skip_binders (n+1)
| KEYWORD ":=" -> ()
| _ -> err () in
- match stream_nth 0 strm with
+ match LStream.peek_nth 0 strm with
| KEYWORD "(" -> skip_binders 2
- | _ -> err ())
+ | _ -> err () })
let lookup_at_as_comma =
let open Pcoq.Lookahead in
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index ad85f68b03..04341fad91 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -249,25 +249,25 @@ let pr_ssrsimpl _ _ _ = pr_simpl
let wit_ssrsimplrep = add_genarg "ssrsimplrep" (fun env sigma -> pr_simpl)
-let test_ssrslashnum b1 b2 _ strm =
- match Util.stream_nth 0 strm with
+let test_ssrslashnum b1 b2 strm =
+ match LStream.peek_nth 0 strm with
| Tok.KEYWORD "/" ->
- (match Util.stream_nth 1 strm with
+ (match LStream.peek_nth 1 strm with
| Tok.NUMBER _ when b1 ->
- (match Util.stream_nth 2 strm with
+ (match LStream.peek_nth 2 strm with
| Tok.KEYWORD "=" | Tok.KEYWORD "/=" when not b2 -> ()
| Tok.KEYWORD "/" ->
if not b2 then () else begin
- match Util.stream_nth 3 strm with
+ match LStream.peek_nth 3 strm with
| Tok.NUMBER _ -> ()
| _ -> raise Stream.Failure
end
| _ -> raise Stream.Failure)
| Tok.KEYWORD "/" when not b1 ->
- (match Util.stream_nth 2 strm with
+ (match LStream.peek_nth 2 strm with
| Tok.KEYWORD "=" when not b2 -> ()
| Tok.NUMBER _ when b2 ->
- (match Util.stream_nth 3 strm with
+ (match LStream.peek_nth 3 strm with
| Tok.KEYWORD "=" -> ()
| _ -> raise Stream.Failure)
| _ when not b2 -> ()
@@ -275,10 +275,10 @@ let test_ssrslashnum b1 b2 _ strm =
| Tok.KEYWORD "=" when not b1 && not b2 -> ()
| _ -> raise Stream.Failure)
| Tok.KEYWORD "//" when not b1 ->
- (match Util.stream_nth 1 strm with
+ (match LStream.peek_nth 1 strm with
| Tok.KEYWORD "=" when not b2 -> ()
| Tok.NUMBER _ when b2 ->
- (match Util.stream_nth 2 strm with
+ (match LStream.peek_nth 2 strm with
| Tok.KEYWORD "=" -> ()
| _ -> raise Stream.Failure)
| _ when not b2 -> ()
@@ -290,23 +290,23 @@ let test_ssrslashnum11 = test_ssrslashnum true true
let test_ssrslashnum01 = test_ssrslashnum false true
let test_ssrslashnum00 = test_ssrslashnum false false
-let negate_parser f tok x =
- let rc = try Some (f tok x) with Stream.Failure -> None in
+let negate_parser f x =
+ let rc = try Some (f x) with Stream.Failure -> None in
match rc with
| None -> ()
| Some _ -> raise Stream.Failure
let test_not_ssrslashnum =
- Pcoq.Entry.of_parser
- "test_not_ssrslashnum" (negate_parser test_ssrslashnum10)
+ Pcoq.Entry.(of_parser
+ "test_not_ssrslashnum" { parser_fun = negate_parser test_ssrslashnum10 })
let test_ssrslashnum00 =
- Pcoq.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum00
+ Pcoq.Entry.(of_parser "test_ssrslashnum01" { parser_fun = test_ssrslashnum00 })
let test_ssrslashnum10 =
- Pcoq.Entry.of_parser "test_ssrslashnum10" test_ssrslashnum10
+ Pcoq.Entry.(of_parser "test_ssrslashnum10" { parser_fun = test_ssrslashnum10 })
let test_ssrslashnum11 =
- Pcoq.Entry.of_parser "test_ssrslashnum11" test_ssrslashnum11
+ Pcoq.Entry.(of_parser "test_ssrslashnum11" { parser_fun = test_ssrslashnum11 })
let test_ssrslashnum01 =
- Pcoq.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum01
+ Pcoq.Entry.(of_parser "test_ssrslashnum01" { parser_fun = test_ssrslashnum01 })
}
@@ -488,23 +488,23 @@ END
(* Old kinds of terms *)
-let input_ssrtermkind _ strm = match Util.stream_nth 0 strm with
+let input_ssrtermkind strm = match LStream.peek_nth 0 strm with
| Tok.KEYWORD "(" -> InParens
| Tok.KEYWORD "@" -> WithAt
| _ -> NoFlag
-let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind
+let ssrtermkind = Pcoq.Entry.(of_parser "ssrtermkind" { parser_fun = input_ssrtermkind })
(* New kinds of terms *)
-let input_term_annotation _ strm =
- match Stream.npeek 2 strm with
+let input_term_annotation strm =
+ match LStream.npeek 2 strm with
| Tok.KEYWORD "(" :: Tok.KEYWORD "(" :: _ -> `DoubleParens
| Tok.KEYWORD "(" :: _ -> `Parens
| Tok.KEYWORD "@" :: _ -> `At
| _ -> `None
let term_annotation =
- Pcoq.Entry.of_parser "term_annotation" input_term_annotation
+ Pcoq.Entry.(of_parser "term_annotation" { parser_fun = input_term_annotation })
(* terms *)
@@ -837,29 +837,29 @@ END
{
-let reject_ssrhid _ strm =
- match Util.stream_nth 0 strm with
+let reject_ssrhid strm =
+ match LStream.peek_nth 0 strm with
| Tok.KEYWORD "[" ->
- (match Util.stream_nth 1 strm with
+ (match LStream.peek_nth 1 strm with
| Tok.KEYWORD ":" -> raise Stream.Failure
| _ -> ())
| _ -> ()
-let test_nohidden = Pcoq.Entry.of_parser "test_ssrhid" reject_ssrhid
+let test_nohidden = Pcoq.Entry.(of_parser "test_ssrhid" { parser_fun = reject_ssrhid })
-let rec reject_binder crossed_paren k tok s =
+let rec reject_binder crossed_paren k s =
match
- try Some (Util.stream_nth k s)
+ try Some (LStream.peek_nth k s)
with Stream.Failure -> None
with
- | Some (Tok.KEYWORD "(") when not crossed_paren -> reject_binder true (k+1) tok s
- | Some (Tok.IDENT _) when crossed_paren -> reject_binder true (k+1) tok s
+ | Some (Tok.KEYWORD "(") when not crossed_paren -> reject_binder true (k+1) s
+ | Some (Tok.IDENT _) when crossed_paren -> reject_binder true (k+1) s
| Some (Tok.KEYWORD ":" | Tok.KEYWORD ":=") when crossed_paren ->
raise Stream.Failure
| Some (Tok.KEYWORD ")") when crossed_paren -> raise Stream.Failure
| _ -> if crossed_paren then () else raise Stream.Failure
-let _test_nobinder = Pcoq.Entry.of_parser "test_nobinder" (reject_binder false 0)
+let _test_nobinder = Pcoq.Entry.(of_parser "test_nobinder" { parser_fun = reject_binder false 0 })
}
@@ -1673,7 +1673,7 @@ let ssr_id_of_string loc s =
^ "Scripts with explicit references to anonymous variables are fragile."))
end; Id.of_string s
-let ssr_null_entry = Pcoq.Entry.of_parser "ssr_null" (fun _ _ -> ())
+let ssr_null_entry = Pcoq.Entry.(of_parser "ssr_null" { parser_fun = fun _ -> () })
}
@@ -2407,13 +2407,13 @@ let lbrace = Char.chr 123
(** Workaround to a limitation of coqpp *)
let test_ssr_rw_syntax =
- let test _ strm =
+ let test strm =
if not !ssr_rw_syntax then raise Stream.Failure else
if is_ssr_loaded () then () else
- match Util.stream_nth 0 strm with
+ match LStream.peek_nth 0 strm with
| Tok.KEYWORD key when List.mem key.[0] [lbrace; '['; '/'] -> ()
| _ -> raise Stream.Failure in
- Pcoq.Entry.of_parser "test_ssr_rw_syntax" test
+ Pcoq.Entry.(of_parser "test_ssr_rw_syntax" { parser_fun = test })
}
diff --git a/plugins/ssrmatching/g_ssrmatching.mlg b/plugins/ssrmatching/g_ssrmatching.mlg
index 7022949ab6..b917e43b7c 100644
--- a/plugins/ssrmatching/g_ssrmatching.mlg
+++ b/plugins/ssrmatching/g_ssrmatching.mlg
@@ -66,11 +66,11 @@ END
{
-let input_ssrtermkind _ strm = match Util.stream_nth 0 strm with
+let input_ssrtermkind strm = match LStream.peek_nth 0 strm with
| Tok.KEYWORD "(" -> InParens
| Tok.KEYWORD "@" -> WithAt
| _ -> NoFlag
-let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind
+let ssrtermkind = Pcoq.Entry.(of_parser "ssrtermkind" { parser_fun = input_ssrtermkind })
}
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-18 04:45:35 +0000