aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/funind/functional_principles_proofs.ml15
-rw-r--r--plugins/funind/glob_term_to_relation.ml4
-rw-r--r--plugins/funind/glob_termops.ml6
-rw-r--r--plugins/funind/indfun.ml2
-rw-r--r--plugins/ltac/rewrite.ml13
-rw-r--r--plugins/omega/coq_omega.ml2
-rw-r--r--plugins/ssr/ssrcommon.ml4
7 files changed, 28 insertions, 18 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 62ca706264..d04887a489 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -324,7 +324,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type =
context
in
let new_type_of_hyp =
- Reductionops.nf_betaiota sigma new_type_of_hyp in
+ Reductionops.nf_betaiota env sigma new_type_of_hyp in
let new_ctxt,new_end_of_type =
decompose_prod_n_assum sigma ctxt_size new_type_of_hyp
in
@@ -698,6 +698,7 @@ let build_proof
: tactic =
let rec build_proof_aux do_finalize dyn_infos : tactic =
fun g ->
+ let env = pf_env g in
let sigma = project g in
(* observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*)
match EConstr.kind sigma dyn_infos.info with
@@ -794,7 +795,7 @@ let build_proof
do_finalize dyn_infos g
| Lambda _ ->
let new_term =
- Reductionops.nf_beta sigma dyn_infos.info in
+ Reductionops.nf_beta env sigma dyn_infos.info in
build_proof do_finalize {dyn_infos with info = new_term}
g
| LetIn _ ->
@@ -1153,7 +1154,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
let bodies_with_all_params =
Array.map
(fun body ->
- Reductionops.nf_betaiota (project g)
+ Reductionops.nf_betaiota (pf_env g) (project g)
(applist(substl (List.rev (Array.to_list all_funs_with_full_params)) body,
List.rev_map var_of_decl princ_params))
)
@@ -1191,12 +1192,12 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
let body_with_param,num =
let body = get_body fnames.(i) in
let body_with_full_params =
- Reductionops.nf_betaiota (project g) (
+ Reductionops.nf_betaiota (pf_env g) (project g) (
applist(body,List.rev_map var_of_decl full_params))
in
match EConstr.kind (project g) body_with_full_params with
| Fix((_,num),(_,_,bs)) ->
- Reductionops.nf_betaiota (project g)
+ Reductionops.nf_betaiota (pf_env g) (project g)
(
(applist
(substl
@@ -1279,7 +1280,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
nb_rec_hyps = -100;
rec_hyps = [];
info =
- Reductionops.nf_betaiota (project g)
+ Reductionops.nf_betaiota (pf_env g) (project g)
(applist(fix_body,List.rev_map mkVar args_id));
eq_hyps = []
}
@@ -1339,7 +1340,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
nb_rec_hyps = -100;
rec_hyps = [];
info =
- Reductionops.nf_betaiota Evd.empty
+ Reductionops.nf_betaiota (pf_env g) Evd.empty
(applist(fbody_with_full_params,
(List.rev_map var_of_decl princ_params)@
(List.rev_map mkVar args_id)
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 0b929b8ca9..f7639d22d6 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -591,6 +591,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
*)
build_entry_lc env funnames avoid (mkGApp(b,args))
| GRec _ -> user_err Pp.(str "Not handled GRec")
+ | GProj _ -> user_err Pp.(str "Funind does not support primitive projections")
| GProd _ -> user_err Pp.(str "Cannot apply a type")
end (* end of the application treatement *)
@@ -697,6 +698,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
| GRec _ -> user_err Pp.(str "Not handled GRec")
| GCast(b,_) ->
build_entry_lc env funnames avoid b
+ | GProj(_,_) -> user_err Pp.(str "Funind does not support primitive projections")
and build_entry_lc_from_case env funname make_discr
(el:tomatch_tuples)
(brl:Glob_term.cases_clauses) avoid :
@@ -1245,7 +1247,7 @@ let rec compute_cst_params relnames params gt = DAst.with_val (function
discrimination ones *)
| GSort _ -> params
| GHole _ -> params
- | GIf _ | GRec _ | GCast _ ->
+ | GIf _ | GRec _ | GCast _ | GProj _ ->
raise (UserError(Some "compute_cst_params", str "Not handled case"))
) gt
and compute_cst_params_from_app acc (params,rtl) =
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index be8abb92e7..b4ca1073ca 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -109,6 +109,7 @@ let change_vars =
| GCast(b,c) ->
GCast(change_vars mapping b,
Miscops.map_cast_type (change_vars mapping) c)
+ | GProj(p,c) -> GProj(p, change_vars mapping c)
) rt
and change_vars_br mapping ((loc,(idl,patl,res)) as br) =
let new_mapping = List.fold_right Id.Map.remove idl mapping in
@@ -293,6 +294,7 @@ let rec alpha_rt excluded rt =
GApp(alpha_rt excluded f,
List.map (alpha_rt excluded) args
)
+ | GProj(p,c) -> GProj(p, alpha_rt excluded c)
in
new_rt
@@ -344,6 +346,7 @@ 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
+ | GProj (_,c) -> is_free_in c
) x
and is_free_in_br (_,(ids,_,rt)) =
(not (Id.List.mem id ids)) && is_free_in rt
@@ -437,6 +440,8 @@ let replace_var_by_term x_id term =
| GCast(b,c) ->
GCast(replace_var_by_pattern b,
Miscops.map_cast_type replace_var_by_pattern c)
+ | GProj(p,c) ->
+ GProj(p,replace_var_by_pattern c)
) x
and replace_var_by_pattern_br ((loc,(idl,patl,res)) as br) =
if List.exists (fun id -> Id.compare id x_id == 0) idl
@@ -540,6 +545,7 @@ let expand_as =
| GCases(sty,po,el,brl) ->
GCases(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)
+ | GProj(p,c) -> GProj(p, expand_as map c)
)
and expand_as_br map (loc,(idl,cpl,rt)) =
(loc,(idl,cpl, expand_as (List.fold_left add_as map cpl) rt))
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 071bab2f3f..58154d3106 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -215,6 +215,7 @@ let is_rec names =
| GCases(_,_,el,brl) ->
List.exists (fun (e,_) -> lookup names e) el ||
List.exists (lookup_br names) brl
+ | GProj(_,c) -> lookup names c
and lookup_br names (_,(idl,_,rt)) =
let new_names = List.fold_right Id.Set.remove idl names in
lookup new_names rt
@@ -779,6 +780,7 @@ let rec add_args id new_args = CAst.map (function
| CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.")
| CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization.")
| CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters.")
+ | CProj _ -> user_err Pp.(str "Funind does not support primitive projections")
)
exception Stop of Constrexpr.constr_expr
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 3cbb110010..acd7a30c43 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -210,9 +210,9 @@ end) = struct
let t = Reductionops.whd_all env (goalevars evars) ty in
match EConstr.kind (goalevars evars) t, l with
| Prod (na, ty, b), obj :: cstrs ->
- let b = Reductionops.nf_betaiota (goalevars evars) b in
+ let b = Reductionops.nf_betaiota env (goalevars evars) b in
if noccurn (goalevars evars) 1 b (* non-dependent product *) then
- let ty = Reductionops.nf_betaiota (goalevars evars) ty in
+ let ty = Reductionops.nf_betaiota env (goalevars evars) ty in
let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in
let evars, relty = mk_relty evars env ty obj in
let evars, newarg = app_poly env evars respectful [| ty ; b' ; relty ; arg |] in
@@ -221,7 +221,7 @@ end) = struct
let (evars, b, arg, cstrs) =
aux (push_rel (LocalAssum (na, ty)) env) evars b cstrs
in
- let ty = Reductionops.nf_betaiota (goalevars evars) ty in
+ let ty = Reductionops.nf_betaiota env (goalevars evars) ty in
let pred = mkLambda (na, ty, b) in
let liftarg = mkLambda (na, ty, arg) in
let evars, arg' = app_poly env evars forall_relation [| ty ; pred ; liftarg |] in
@@ -231,7 +231,7 @@ end) = struct
| _, [] ->
(match finalcstr with
| None | Some (_, None) ->
- let t = Reductionops.nf_betaiota (fst evars) ty in
+ let t = Reductionops.nf_betaiota env (fst evars) ty in
let evars, rel = mk_relty evars env t None in
evars, t, rel, [t, Some rel]
| Some (t, Some rel) -> evars, t, rel, [t, Some rel])
@@ -1557,9 +1557,8 @@ let newfail n s =
let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
let open Proofview.Notations in
(** For compatibility *)
- let beta_red _ sigma c = Reductionops.nf_betaiota sigma c in
- let beta = Tactics.reduct_in_concl (beta_red, DEFAULTcast) in
- let beta_hyp id = Tactics.reduct_in_hyp beta_red (id, InHyp) in
+ let beta = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in
+ let beta_hyp id = Tactics.reduct_in_hyp Reductionops.nf_betaiota (id, InHyp) in
let treat sigma res =
match res with
| None -> newfail 0 (str "Nothing to rewrite")
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 8692842468..4271c80cd1 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -652,7 +652,7 @@ let decompile af =
(** Backward compat to emulate the old Refine: normalize the goal conclusion *)
let new_hole env sigma c =
- let c = Reductionops.nf_betaiota sigma c in
+ let c = Reductionops.nf_betaiota env sigma c in
Evarutil.new_evar env sigma c
let clever_rewrite_base_poly typ p result theorem =
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 8493dbdbb5..7cdf051176 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -563,7 +563,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) =
| _ -> Constr.fold put evlist c in
let evlist = put [] c0 in
if evlist = [] then 0, c0 else
- let pr_constr t = Printer.pr_econstr_env (pf_env gl) sigma (Reductionops.nf_beta (project gl) (EConstr.of_constr t)) in
+ let pr_constr t = Printer.pr_econstr_env (pf_env gl) sigma (Reductionops.nf_beta (pf_env gl) (project gl) (EConstr.of_constr t)) in
pp(lazy(str"evlist=" ++ pr_list (fun () -> str";")
(fun (k,_) -> Evar.print k) evlist));
let evplist =
@@ -894,7 +894,7 @@ let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_
let sigma = create_evar_defs sigma in
let (sigma, x) =
Evarutil.new_evar env sigma
- (if bi_types then Reductionops.nf_betaiota sigma src else src) in
+ (if bi_types then Reductionops.nf_betaiota env sigma src else src) in
loop (EConstr.Vars.subst1 x tgt) ((m - n,x) :: args) sigma (n-1)
| CastType (t, _) -> loop t args sigma n
| LetInType (_, v, _, t) -> loop (EConstr.Vars.subst1 v t) args sigma n
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 23:56:11 +0000