aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/common.ml5
-rw-r--r--plugins/extraction/common.mli1
-rw-r--r--plugins/extraction/extraction.ml8
-rw-r--r--plugins/extraction/haskell.ml2
-rw-r--r--plugins/extraction/json.ml5
-rw-r--r--plugins/extraction/miniml.ml1
-rw-r--r--plugins/extraction/miniml.mli1
-rw-r--r--plugins/extraction/mlutil.ml11
-rw-r--r--plugins/extraction/modutil.ml2
-rw-r--r--plugins/extraction/ocaml.ml5
-rw-r--r--plugins/extraction/scheme.ml2
-rw-r--r--plugins/funind/functional_principles_proofs.ml5
-rw-r--r--plugins/funind/gen_principle.ml15
-rw-r--r--plugins/funind/glob_term_to_relation.ml4
-rw-r--r--plugins/funind/glob_termops.ml29
-rw-r--r--plugins/funind/recdef.ml20
-rw-r--r--plugins/ltac/g_obligations.mlg22
-rw-r--r--plugins/ssr/ssrast.mli8
-rw-r--r--plugins/ssr/ssrcommon.ml13
-rw-r--r--plugins/ssr/ssrelim.ml1
-rw-r--r--plugins/ssr/ssrview.ml10
-rw-r--r--plugins/ssrmatching/ssrmatching.ml1
22 files changed, 133 insertions, 38 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 0dbc0513b4..4a41f4c890 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -63,6 +63,11 @@ let pp_boxed_tuple f = function
| [x] -> f x
| l -> pp_par true (hov 0 (prlist_with_sep (fun () -> str "," ++ spc ()) f l))
+let pp_array f = function
+ | [] -> mt ()
+ | [x] -> f x
+ | l -> pp_par true (prlist_with_sep (fun () -> str ";" ++ spc ()) f l)
+
(** By default, in module Format, you can do horizontal placing of blocks
even if they include newlines, as long as the number of chars in the
blocks is less that a line length. To avoid this awkward situation,
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index e77d37fb81..0bd9efd255 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -30,6 +30,7 @@ val pp_apply2 : Pp.t -> bool -> Pp.t list -> Pp.t
val pp_tuple_light : (bool -> 'a -> Pp.t) -> 'a list -> Pp.t
val pp_tuple : ('a -> Pp.t) -> 'a list -> Pp.t
+val pp_array : ('a -> Pp.t) -> 'a list -> Pp.t
val pp_boxed_tuple : ('a -> Pp.t) -> 'a list -> Pp.t
val pr_binding : Id.t list -> Pp.t
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index a7c926f50c..2dca1d5e49 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -351,7 +351,7 @@ let rec extract_type env sg db j c args =
| (Info, TypeScheme) ->
extract_type_app env sg db (r, type_sign env sg ty) args
| (Info, Default) -> Tunknown))
- | Cast _ | LetIn _ | Construct _ | Int _ | Float _ -> assert false
+ | Cast _ | LetIn _ | Construct _ | Int _ | Float _ | Array _ -> assert false
(*s Auxiliary function dealing with type application.
Precondition: [r] is a type scheme represented by the signature [s],
@@ -693,6 +693,12 @@ let rec extract_term env sg mle mlt c args =
extract_app env sg mle mlt extract_var args
| Int i -> assert (args = []); MLuint i
| Float f -> assert (args = []); MLfloat f
+ | Array (_u,t,def,_ty) ->
+ assert (args = []);
+ let a = new_meta () in
+ let ml_arr = Array.map (fun c -> extract_term env sg mle a c []) t in
+ let def = extract_term env sg mle a def [] in
+ MLparray(ml_arr, def)
| Ind _ | Prod _ | Sort _ -> assert false
(*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *)
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 97fe8a5776..c25285c987 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -218,6 +218,8 @@ let rec pp_expr par env args =
pp_par par (str "Prelude.error \"EXTRACTION OF UINT NOT IMPLEMENTED\"")
| MLfloat _ ->
pp_par par (str "Prelude.error \"EXTRACTION OF FLOAT NOT IMPLEMENTED\"")
+ | MLparray _ ->
+ pp_par par (str "Prelude.error \"EXTRACTION OF ARRAY NOT IMPLEMENTED\"")
and pp_cons_pat par r ppl =
pp_par par
diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml
index 81b3e1bcdc..974d254d9c 100644
--- a/plugins/extraction/json.ml
+++ b/plugins/extraction/json.ml
@@ -165,6 +165,11 @@ let rec json_expr env = function
("what", json_str "expr:float");
("float", json_str (Float64.to_string f))
]
+ | MLparray(t,def) -> json_dict [
+ ("what", json_str "expr:array");
+ ("elems", json_listarr (Array.map (json_expr env) t));
+ ("default", json_expr env def)
+ ]
and json_one_pat env (ids,p,t) =
let ids', env' = push_vars (List.rev_map id_of_mlid ids) env in json_dict [
diff --git a/plugins/extraction/miniml.ml b/plugins/extraction/miniml.ml
index 451272d554..a5a6564873 100644
--- a/plugins/extraction/miniml.ml
+++ b/plugins/extraction/miniml.ml
@@ -128,6 +128,7 @@ and ml_ast =
| MLmagic of ml_ast
| MLuint of Uint63.t
| MLfloat of Float64.t
+ | MLparray of ml_ast array * ml_ast
and ml_pattern =
| Pcons of GlobRef.t * ml_pattern list
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index 451272d554..a5a6564873 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -128,6 +128,7 @@ and ml_ast =
| MLmagic of ml_ast
| MLuint of Uint63.t
| MLfloat of Float64.t
+ | MLparray of ml_ast array * ml_ast
and ml_pattern =
| Pcons of GlobRef.t * ml_pattern list
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 465ad50e9b..b1ce10985a 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -431,6 +431,7 @@ let ast_iter_rel f =
| MLapp (a,l) -> iter n a; List.iter (iter n) l
| MLcons (_,_,l) | MLtuple l -> List.iter (iter n) l
| MLmagic a -> iter n a
+ | MLparray (t,def) -> Array.iter (iter n) t; iter n def
| MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ | MLfloat _ -> ()
in iter 0
@@ -450,6 +451,7 @@ let ast_map f = function
| MLcons (typ,c,l) -> MLcons (typ,c, List.map f l)
| MLtuple l -> MLtuple (List.map f l)
| MLmagic a -> MLmagic (f a)
+ | MLparray (t,def) -> MLparray (Array.map f t, f def)
| MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom
| MLuint _ | MLfloat _ as a -> a
@@ -469,6 +471,7 @@ let ast_map_lift f n = function
| MLcons (typ,c,l) -> MLcons (typ,c, List.map (f n) l)
| MLtuple l -> MLtuple (List.map (f n) l)
| MLmagic a -> MLmagic (f n a)
+ | MLparray (t,def) -> MLparray (Array.map (f n) t, f n def)
| MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom
| MLuint _ | MLfloat _ as a -> a
@@ -484,6 +487,7 @@ let ast_iter f = function
| MLapp (a,l) -> f a; List.iter f l
| MLcons (_,_,l) | MLtuple l -> List.iter f l
| MLmagic a -> f a
+ | MLparray (t,def) -> Array.iter f t; f def
| MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom
| MLuint _ | MLfloat _ -> ()
@@ -521,6 +525,7 @@ let nb_occur_match =
| MLapp (a,l) -> List.fold_left (fun r a -> r+(nb k a)) (nb k a) l
| MLcons (_,_,l) | MLtuple l -> List.fold_left (fun r a -> r+(nb k a)) 0 l
| MLmagic a -> nb k a
+ | MLparray (t,def) -> Array.fold_left (fun r a -> r+(nb k a)) 0 t + nb k def
| MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ | MLfloat _ -> 0
in nb 1
@@ -573,6 +578,11 @@ let dump_unused_vars a =
let b' = ren env b in
if b' == b then a else MLmagic b'
+ | MLparray(t,def) ->
+ let t' = Array.Smart.map (ren env) t in
+ let def' = ren env def in
+ if def' == def && t' == t then a else MLparray(t',def')
+
| MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ | MLfloat _ -> a
and ren_branch env ((ids,p,b) as tr) =
@@ -1406,6 +1416,7 @@ let rec ml_size = function
| MLfix(_,_,f) -> ml_size_array f
| MLletin (_,_,t) -> ml_size t
| MLmagic t -> ml_size t
+ | MLparray(t,def) -> ml_size_array t + ml_size def
| MLglob _ | MLrel _ | MLexn _ | MLdummy _ | MLaxiom
| MLuint _ | MLfloat _ -> 0
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index d051602844..3a481039bf 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -107,7 +107,7 @@ let ast_iter_references do_term do_cons do_type a =
Array.iter (fun (_,p,_) -> patt_iter_references do_cons p) v
| MLrel _ | MLlam _ | MLapp _ | MLletin _ | MLtuple _ | MLfix _ | MLexn _
- | MLdummy _ | MLaxiom | MLmagic _ | MLuint _ | MLfloat _ -> ()
+ | MLdummy _ | MLaxiom | MLmagic _ | MLuint _ | MLfloat _ | MLparray _ -> ()
in iter a
let ind_iter_references do_term do_cons do_type kn ind =
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index a2ce47b11f..088405da5d 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -311,6 +311,11 @@ let rec pp_expr par env args =
| MLfloat f ->
assert (args=[]);
str "(" ++ str (Float64.compile f) ++ str ")"
+ | MLparray(t,def) ->
+ assert (args=[]);
+ let tuple = pp_array (pp_expr true env []) (Array.to_list t) in
+ let def = pp_expr true env [] def in
+ str "(ExtrNative.of_array [|" ++ tuple ++ str "|]" ++ spc () ++ def ++ str")"
and pp_record_proj par env typ t pv args =
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 1fb605fc9a..ee50476b10 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -133,6 +133,8 @@ let rec pp_expr env args =
paren (str "Prelude.error \"EXTRACTION OF UINT NOT IMPLEMENTED\"")
| MLfloat _ ->
paren (str "Prelude.error \"EXTRACTION OF FLOAT NOT IMPLEMENTED\"")
+ | MLparray _ ->
+ paren (str "Prelude.error \"EXTRACTION OF PARRAY NOT IMPLEMENTED\"")
and pp_cons_args env = function
| MLcons (_,r,args) when is_coinductive r ->
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index f2658a395f..743afe4177 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -645,6 +645,7 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos
match EConstr.kind sigma f with
| Int _ -> user_err Pp.(str "integer cannot be applied")
| Float _ -> user_err Pp.(str "float cannot be applied")
+ | Array _ -> user_err Pp.(str "array cannot be applied")
| App _ ->
assert false (* we have collected all the app in decompose_app *)
| Proj _ -> assert false (*FIXME*)
@@ -696,6 +697,7 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos
; build_proof do_finalize new_infos ]
g
| Rel _ -> anomaly (Pp.str "Free var in goal conclusion!")
+ | Array _ -> CErrors.user_err Pp.(str "Arrays not handled yet")
and build_proof do_finalize dyn_infos g =
(* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *)
Indfun_common.observe_tac
@@ -862,7 +864,8 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
Declare.Proof.by (Proofview.V82.tactic prove_replacement) lemma
in
let (_ : _ list) =
- Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None
+ Declare.Proof.save_regular ~proof:lemma ~opaque:Vernacexpr.Transparent
+ ~idopt:None
in
evd
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index f773157c52..45b1713441 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -103,6 +103,8 @@ let is_rec names =
names nal)
b
| GApp (f, args) -> List.exists (lookup names) (f :: args)
+ | GArray (_u, t, def, ty) ->
+ Array.exists (lookup names) t || lookup names def || lookup names ty
| GCases (_, _, el, brl) ->
List.exists (fun (e, _) -> lookup names e) el
|| List.exists (lookup_br names) brl
@@ -1524,9 +1526,9 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
let lemma =
fst @@ Declare.Proof.by (Proofview.V82.tactic (proving_tac i)) lemma
in
- let (_ : GlobRef.t list) =
- Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent
- ~idopt:None
+ let (_ : _ list) =
+ Declare.Proof.save_regular ~proof:lemma
+ ~opaque:Vernacexpr.Transparent ~idopt:None
in
let finfo =
match find_Function_infos (fst f_as_constant) with
@@ -1597,8 +1599,8 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
lemma)
in
let (_ : _ list) =
- Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent
- ~idopt:None
+ Declare.Proof.save_regular ~proof:lemma
+ ~opaque:Vernacexpr.Transparent ~idopt:None
in
let finfo =
match find_Function_infos (fst f_as_constant) with
@@ -2047,7 +2049,8 @@ let rec add_args id new_args =
| CGeneralization _ ->
CErrors.anomaly ~label:"add_args " (Pp.str "CGeneralization.")
| CDelimiters _ ->
- CErrors.anomaly ~label:"add_args " (Pp.str "CDelimiters."))
+ CErrors.anomaly ~label:"add_args " (Pp.str "CDelimiters.")
+ | CArray _ -> CErrors.anomaly ~label:"add_args " (Pp.str "CArray."))
let rec get_args b t :
Constrexpr.local_binder_expr list
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 11e4fa0ac7..6ed61043f9 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -568,6 +568,7 @@ let rec build_entry_lc env sigma funnames avoid rt :
| GProd _ -> user_err Pp.(str "Cannot apply a type")
| GInt _ -> user_err Pp.(str "Cannot apply an integer")
| GFloat _ -> user_err Pp.(str "Cannot apply a float")
+ | GArray _ -> user_err Pp.(str "Cannot apply an array")
(* end of the application treatement *) )
| GLambda (n, _, t, b) ->
(* we first compute the list of constructor
@@ -672,6 +673,7 @@ let rec build_entry_lc env sigma funnames avoid rt :
build_entry_lc env sigma funnames avoid match_expr
| GRec _ -> user_err Pp.(str "Not handled GRec")
| GCast (b, _) -> build_entry_lc env sigma funnames avoid b
+ | GArray _ -> user_err Pp.(str "Not handled GArray")
and build_entry_lc_from_case env sigma funname make_discr (el : tomatch_tuples)
(brl : Glob_term.cases_clauses) avoid : glob_constr build_entry_return =
@@ -1196,7 +1198,7 @@ let rec compute_cst_params relnames params gt =
discrimination ones *)
| GSort _ -> params
| GHole _ -> params
- | GIf _ | GRec _ | GCast _ ->
+ | GIf _ | GRec _ | GCast _ | GArray _ ->
CErrors.user_err ~hdr:"compute_cst_params" (str "Not handled case"))
gt
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 5026120849..8e1331ace9 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -109,7 +109,13 @@ let change_vars =
| GCast (b, c) ->
GCast
( change_vars mapping b
- , Glob_ops.map_cast_type (change_vars mapping) c ))
+ , Glob_ops.map_cast_type (change_vars mapping) c )
+ | GArray (u, t, def, ty) ->
+ GArray
+ ( u
+ , Array.map (change_vars mapping) t
+ , change_vars mapping def
+ , change_vars mapping ty ))
rt
and change_vars_br mapping ({CAst.loc; v = idl, patl, res} as br) =
let new_mapping = List.fold_right Id.Map.remove idl mapping in
@@ -282,6 +288,12 @@ let rec alpha_rt excluded rt =
GCast (alpha_rt excluded b, Glob_ops.map_cast_type (alpha_rt excluded) c)
| GApp (f, args) ->
GApp (alpha_rt excluded f, List.map (alpha_rt excluded) args)
+ | GArray (u, t, def, ty) ->
+ GArray
+ ( u
+ , Array.map (alpha_rt excluded) t
+ , alpha_rt excluded def
+ , alpha_rt excluded ty )
in
new_rt
@@ -331,7 +343,9 @@ let is_free_in id =
| 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
- | GInt _ | GFloat _ -> false)
+ | GInt _ | GFloat _ -> false
+ | GArray (_u, t, def, ty) ->
+ Array.exists is_free_in t || is_free_in def || is_free_in ty)
x
and is_free_in_br {CAst.v = ids, _, rt} =
(not (Id.List.mem id ids)) && is_free_in rt
@@ -404,6 +418,12 @@ let replace_var_by_term x_id term =
| (GSort _ | GHole _) as rt -> rt
| GInt _ as rt -> rt
| GFloat _ as rt -> rt
+ | GArray (u, t, def, ty) ->
+ GArray
+ ( u
+ , Array.map replace_var_by_pattern t
+ , replace_var_by_pattern def
+ , replace_var_by_pattern ty )
| GCast (b, c) ->
GCast
( replace_var_by_pattern b
@@ -510,7 +530,10 @@ let expand_as =
( sty
, Option.map (expand_as map) po
, List.map (fun (rt, t) -> (expand_as map rt, t)) el
- , List.map (expand_as_br map) brl ))
+ , List.map (expand_as_br map) brl )
+ | GArray (u, t, def, ty) ->
+ GArray
+ (u, Array.map (expand_as map) t, expand_as map def, expand_as map ty))
and expand_as_br map {CAst.loc; v = idl, cpl, rt} =
CAst.make ?loc (idl, cpl, expand_as (List.fold_left add_as map cpl) rt)
in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 701ea56c2a..253c95fa67 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -59,7 +59,8 @@ let declare_fun name kind ?univs value =
let defined lemma =
let (_ : _ list) =
- Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None
+ Declare.Proof.save_regular ~proof:lemma ~opaque:Vernacexpr.Transparent
+ ~idopt:None
in
()
@@ -305,9 +306,11 @@ let check_not_nested env sigma forbidden e =
| Lambda (_, t, b) -> check_not_nested t; check_not_nested b
| LetIn (_, v, t, b) ->
check_not_nested t; check_not_nested b; check_not_nested v
- | App (f, l) ->
- check_not_nested f;
- Array.iter check_not_nested l
+ | App (f, l) -> check_not_nested f
+ | Array (_u, t, def, ty) ->
+ Array.iter check_not_nested t;
+ check_not_nested def;
+ check_not_nested ty
| Proj (p, c) -> check_not_nested c
| Const _ -> ()
| Ind _ -> ()
@@ -447,6 +450,7 @@ let rec travel_aux jinfo continuation_tac (expr_info : constr infos) g =
match EConstr.kind sigma expr_info.info with
| CoFix _ | Fix _ ->
user_err Pp.(str "Function cannot treat local fixpoint or cofixpoint")
+ | Array _ -> user_err Pp.(str "Function cannot treat arrays")
| Proj _ -> user_err Pp.(str "Function cannot treat projections")
| LetIn (na, b, t, e) ->
let new_continuation_tac =
@@ -1500,7 +1504,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
in
let lemma = build_proof env (Evd.from_env env) start_tac end_tac in
let (_ : _ list) =
- Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None
+ Declare.Proof.save_regular ~proof:lemma ~opaque:opacity ~idopt:None
in
()
in
@@ -1659,7 +1663,11 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
in
let _ =
Flags.silently
- (fun () -> Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None)
+ (fun () ->
+ let (_ : _ list) =
+ Declare.Proof.save_regular ~proof:lemma ~opaque:opacity ~idopt:None
+ in
+ ())
()
in
()
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index 81ee6ed5bb..fa176482bf 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -80,14 +80,14 @@ GRAMMAR EXTEND Gram
open Declare.Obls
-let obligation obl tac = with_tac (fun t -> obligation obl t) tac
-let next_obligation obl tac = with_tac (fun t -> next_obligation obl t) tac
+let obligation ~pm obl tac = with_tac (fun t -> obligation ~pm obl t) tac
+let next_obligation ~pm obl tac = with_tac (fun t -> next_obligation ~pm obl t) tac
let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]))
}
-VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE open_proof
+VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE declare_program
| [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
{ obligation (num, Some name, Some t) tac }
| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
@@ -101,14 +101,14 @@ VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE open_pro
| [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac }
END
-VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF
+VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF STATE program
| [ "Solve" "Obligation" integer(num) "of" ident(name) "with" tactic(t) ] ->
{ try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) }
| [ "Solve" "Obligation" integer(num) "with" tactic(t) ] ->
{ try_solve_obligation num None (Some (Tacinterp.interp t)) }
END
-VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF
+VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF STATE program
| [ "Solve" "Obligations" "of" ident(name) "with" tactic(t) ] ->
{ try_solve_obligations (Some name) (Some (Tacinterp.interp t)) }
| [ "Solve" "Obligations" "with" tactic(t) ] ->
@@ -117,14 +117,14 @@ VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF
{ try_solve_obligations None None }
END
-VERNAC COMMAND EXTEND Solve_All_Obligations CLASSIFIED AS SIDEFF
+VERNAC COMMAND EXTEND Solve_All_Obligations CLASSIFIED AS SIDEFF STATE program
| [ "Solve" "All" "Obligations" "with" tactic(t) ] ->
{ solve_all_obligations (Some (Tacinterp.interp t)) }
| [ "Solve" "All" "Obligations" ] ->
{ solve_all_obligations None }
END
-VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF
+VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF STATE program
| [ "Admit" "Obligations" "of" ident(name) ] -> { admit_obligations (Some name) }
| [ "Admit" "Obligations" ] -> { admit_obligations None }
END
@@ -148,14 +148,14 @@ VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY
Feedback.msg_notice (str"Program obligation tactic is " ++ print_default_tactic ()) }
END
-VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY
+VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY STATE read_program
| [ "Obligations" "of" ident(name) ] -> { show_obligations (Some name) }
| [ "Obligations" ] -> { show_obligations None }
END
-VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY
-| [ "Preterm" "of" ident(name) ] -> { Feedback.msg_notice (show_term (Some name)) }
-| [ "Preterm" ] -> { Feedback.msg_notice (show_term None) }
+VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY STATE read_program
+| [ "Preterm" "of" ident(name) ] -> { fun ~pm -> Feedback.msg_notice (show_term ~pm (Some name)) }
+| [ "Preterm" ] -> { fun ~pm -> Feedback.msg_notice (show_term ~pm None) }
END
{
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index 8adffdc709..f6a741f468 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -51,13 +51,19 @@ type ssrterm = ssrtermkind * Genintern.glob_constr_and_expr
(* NEW ssr term *)
+type ast_glob_env = {
+ ast_ltacvars : Id.Set.t;
+ ast_extra : Genintern.Store.t;
+ ast_intern_sign : Genintern.intern_variable_status;
+}
+
(* These terms are raw but closed with the intenalization/interpretation
* context. It is up to the tactic receiving it to decide if such contexts
* are useful or not, and eventually manipulate the term before turning it
* into a constr *)
type ast_closure_term = {
body : Constrexpr.constr_expr;
- glob_env : Genintern.glob_sign option; (* for Tacintern.intern_constr *)
+ glob_env : ast_glob_env option; (* for Tacintern.intern_constr *)
interp_env : Geninterp.interp_sign option; (* for Tacinterp.interp_open_constr_with_bindings *)
annotation : [ `None | `Parens | `DoubleParens | `At ];
}
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 5f463f8de4..1b7768852e 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -302,6 +302,11 @@ let mk_ast_closure_term a t = {
}
let glob_ast_closure_term (ist : Genintern.glob_sign) t =
+ let ist = {
+ ast_ltacvars = ist.Genintern.ltacvars;
+ ast_intern_sign = ist.Genintern.intern_sign;
+ ast_extra = ist.Genintern.extra;
+ } in
{ t with glob_env = Some ist }
let subst_ast_closure_term (_s : Mod_subst.substitution) t =
(* _s makes sense only for glob constr *)
@@ -1124,8 +1129,7 @@ let tclDO n tac =
let _, info = Exninfo.capture e in
let e' = CErrors.UserError (l, prefix i ++ s) in
Exninfo.iraise (e', info)
- | Gramlib.Ploc.Exc(loc, CErrors.UserError (l, s)) ->
- raise (Gramlib.Ploc.Exc(loc, CErrors.UserError (l, prefix i ++ s))) in
+ in
let rec loop i gl =
if i = n then tac_err_at i gl else
(tclTHEN (tac_err_at i) (loop (i + 1))) gl in
@@ -1351,9 +1355,8 @@ let unsafe_intro env decl b =
let inst = List.map (get_id %> EConstr.mkVar) (Environ.named_context env) in
let ninst = EConstr.mkRel 1 :: inst in
let nb = EConstr.Vars.subst1 (EConstr.mkVar (get_id decl)) b in
- let sigma, ev =
- Evarutil.new_evar_instance nctx sigma nb ~principal:true ninst in
- sigma, EConstr.mkNamedLambda_or_LetIn decl ev
+ let sigma, ev = Evarutil.new_pure_evar ~principal:true nctx sigma nb in
+ sigma, EConstr.mkNamedLambda_or_LetIn decl (EConstr.mkEvar (ev, ninst))
end
let set_decl_id id = let open Context in function
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index a12b4aad11..1c81fbc10b 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -490,7 +490,6 @@ let equality_inj l b id c =
let msg = ref "" in
try Proofview.V82.of_tactic (Equality.inj None l b None c) gl
with
- | Gramlib.Ploc.Exc(_,CErrors.UserError (_,s))
| CErrors.UserError (_,s)
when msg := Pp.string_of_ppcmds s;
!msg = "Not a projectable equality but a discriminable one." ||
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index ad0a31622c..d99ead139d 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -150,7 +150,15 @@ let is_tac_in_term ?extra_scope { annotation; body; glob_env; interp_env } =
let sigma = sigma goal in
let ist = Ssrcommon.option_assert_get glob_env (Pp.str"not a term") in
(* We use the env of the goal, not the global one *)
- let ist = { ist with Genintern.genv } in
+ let ist =
+ let open Genintern in
+ {
+ ltacvars = ist.ast_ltacvars;
+ extra = ist.ast_extra;
+ intern_sign = ist.ast_intern_sign;
+ genv;
+ }
+ in
(* We open extra_scope *)
let body =
match extra_scope with
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 1ed632f03f..5dedae6388 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -312,6 +312,7 @@ let iter_constr_LR f c = match kind c with
| Fix (_, (_, t, b)) | CoFix (_, (_, t, b)) ->
for i = 0 to Array.length t - 1 do f t.(i); f b.(i) done
| Proj(_,a) -> f a
+ | Array(_u,t,def,ty) -> Array.iter f t; f def; f ty
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _
| Int _ | Float _) -> ()
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 10:57:32 +0000