aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/btauto/refl_btauto.ml4
-rw-r--r--plugins/extraction/extraction.ml18
-rw-r--r--plugins/firstorder/unify.ml11
-rw-r--r--plugins/funind/functional_principles_proofs.ml4
-rw-r--r--plugins/funind/gen_principle.ml4
-rw-r--r--plugins/funind/recdef.ml12
-rw-r--r--plugins/ltac/extratactics.mlg2
-rw-r--r--plugins/ltac/rewrite.ml14
-rw-r--r--plugins/ssrmatching/ssrmatching.ml5
9 files changed, 44 insertions, 30 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index ac2058ba1b..343fb0b1fe 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -112,13 +112,13 @@ module Bool = struct
else if head === negb && Array.length args = 1 then
Negb (aux args.(0))
else Var (Env.add env c)
- | Case (info, r, _iv, arg, pats) ->
+ | Case (info, _, _, _, _, arg, pats) ->
let is_bool =
let i = info.ci_ind in
Names.Ind.CanOrd.equal i (Lazy.force ind)
in
if is_bool then
- Ifb ((aux arg), (aux pats.(0)), (aux pats.(1)))
+ Ifb ((aux arg), (aux (snd pats.(0))), (aux (snd pats.(1))))
else
Var (Env.add env c)
| _ ->
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 6869f9c47e..0cad192332 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -672,9 +672,11 @@ let rec extract_term env sg mle mlt c args =
(* we unify it with an fresh copy of the stored type of [Rel n]. *)
let extract_rel mlt = put_magic (mlt, Mlenv.get mle n) (MLrel n)
in extract_app env sg mle mlt extract_rel args
- | Case ({ci_ind=ip},_,iv,c0,br) ->
- (* If invert_case then this is a match that will get erased later, but right now we don't care. *)
- extract_app env sg mle mlt (extract_case env sg mle (ip,c0,br)) args
+ | Case (ci, u, pms, r, iv, c0, br) ->
+ (* If invert_case then this is a match that will get erased later, but right now we don't care. *)
+ let (ip, r, iv, c0, br) = EConstr.expand_case env sg (ci, u, pms, r, iv, c0, br) in
+ let ip = ci.ci_ind in
+ extract_app env sg mle mlt (extract_case env sg mle (ip,c0,br)) args
| Fix ((_,i),recd) ->
extract_app env sg mle mlt (extract_fix env sg mle i recd) args
| CoFix (i,recd) ->
@@ -1078,9 +1080,13 @@ let fake_match_projection env p =
let kn = Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg:arg lab in
fold (arg+1) (j+1) (mkProj (Projection.make kn false, mkRel 1)::subst) rem
else
- let p = mkLambda (x, lift 1 indty, liftn 1 2 ty) in
- let branch = lift 1 (it_mkLambda_or_LetIn (mkRel (List.length ctx - (j-1))) ctx) in
- let body = mkCase (ci, p, NoInvert, mkRel 1, [|branch|]) in
+ let p = ([|x|], liftn 1 2 ty) in
+ let branch =
+ let nas = Array.of_list (List.rev_map Context.Rel.Declaration.get_annot ctx) in
+ (nas, mkRel (List.length ctx - (j - 1)))
+ in
+ let params = Context.Rel.to_extended_vect mkRel 1 paramslet in
+ let body = mkCase (ci, u, params, p, NoInvert, mkRel 1, [|branch|]) in
it_mkLambda_or_LetIn (mkLambda (x,indty,body)) mib.mind_params_ctxt
| LocalDef (_,c,t) :: rem ->
let c = liftn 1 j c in
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index c62bc73e41..e208ba9a5c 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -67,10 +67,13 @@ let unif env evd t1 t2=
| _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast evd nt2) bige
| (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))->
Queue.add (a,c) bige;Queue.add (pop b,pop d) bige
- | Case (_,pa,_,ca,va),Case (_,pb,_,cb,vb)->
- Queue.add (pa,pb) bige;
- Queue.add (ca,cb) bige;
- let l=Array.length va in
+ | Case (cia,ua,pmsa,pa,iva,ca,va),Case (cib,ub,pmsb,pb,ivb,cb,vb)->
+ let env = Global.env () in
+ let (cia,pa,iva,ca,va) = EConstr.expand_case env evd (cia,ua,pmsa,pa,iva,ca,va) in
+ let (cib,pb,iva,cb,vb) = EConstr.expand_case env evd (cib,ub,pmsb,pb,ivb,cb,vb) in
+ Queue.add (pa,pb) bige;
+ Queue.add (ca,cb) bige;
+ let l=Array.length va in
if not (Int.equal l (Array.length vb)) then
raise (UFAIL (nt1,nt2))
else
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 67b6839b6e..3234d40f73 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -598,12 +598,12 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos
let sigma = Proofview.Goal.sigma g in
(* observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*)
match EConstr.kind sigma dyn_infos.info with
- | Case (ci, ct, iv, t, cb) ->
+ | Case (ci, u, pms, ct, iv, t, cb) ->
let do_finalize_t dyn_info' =
Proofview.Goal.enter (fun g ->
let t = dyn_info'.info in
let dyn_infos =
- {dyn_info' with info = mkCase (ci, ct, iv, t, cb)}
+ {dyn_info' with info = mkCase (ci, u, pms, ct, iv, t, cb)}
in
let g_nb_prod =
nb_prod (Proofview.Goal.sigma g) (Proofview.Goal.concl g)
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index c344fdd611..cbdebb7bbc 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -972,7 +972,7 @@ and intros_with_rewrite_aux () : unit Proofview.tactic =
( UnivGen.constr_of_monomorphic_global
@@ Coqlib.lib_ref "core.False.type" )) ->
tauto
- | Case (_, _, _, v, _) ->
+ | Case (_, _, _, _, _, v, _) ->
tclTHENLIST [simplest_case v; intros_with_rewrite ()]
| LetIn _ ->
tclTHENLIST
@@ -1005,7 +1005,7 @@ let rec reflexivity_with_destruct_cases () =
(snd (destApp (Proofview.Goal.sigma g) (Proofview.Goal.concl g))).(
2)
with
- | Case (_, _, _, v, _) ->
+ | Case (_, _, _, _, _, v, _) ->
tclTHENLIST
[ simplest_case v
; intros
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 9d896e9182..9e9444951f 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -301,10 +301,11 @@ let check_not_nested env sigma forbidden e =
| Const _ -> ()
| Ind _ -> ()
| Construct _ -> ()
- | Case (_, t, _, e, a) ->
+ | Case (_, _, pms, (_, t), _, e, a) ->
+ Array.iter check_not_nested pms;
check_not_nested t;
check_not_nested e;
- Array.iter check_not_nested a
+ Array.iter (fun (_, c) -> check_not_nested c) a
| Fix _ -> user_err Pp.(str "check_not_nested : Fix")
| CoFix _ -> user_err Pp.(str "check_not_nested : Fix")
in
@@ -367,7 +368,7 @@ type journey_info =
-> unit Proofview.tactic)
-> ( case_info
* constr
- * (constr, EInstance.t) case_invert
+ * case_invert
* constr
* constr array
, constr )
@@ -472,7 +473,8 @@ let rec travel_aux jinfo continuation_tac (expr_info : constr infos) =
++ Printer.pr_leconstr_env env sigma expr_info.info
++ str " can not contain a recursive call to "
++ Id.print expr_info.f_id ) )
- | Case (ci, t, iv, a, l) ->
+ | Case (ci, u, pms, t, iv, a, l) ->
+ let (ci, t, iv, a, l) = EConstr.expand_case env sigma (ci, u, pms, t, iv, a, l) in
let continuation_tac_a =
jinfo.casE (travel jinfo) (ci, t, iv, a, l) expr_info continuation_tac
in
@@ -776,7 +778,7 @@ let terminate_case next_step (ci, a, iv, t, l) expr_info continuation_tac infos
let a' = infos.info in
let new_info =
{ infos with
- info = mkCase (ci, a, iv, a', l)
+ info = mkCase (EConstr.contract_case env sigma (ci, a, iv, a', l))
; is_main_branch = expr_info.is_main_branch
; is_final = expr_info.is_final }
in
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 4a2c298caa..90c366ed63 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -774,7 +774,7 @@ let rec find_a_destructable_match sigma t =
let cl = [cl, (None, None), None], None in
let dest = TacAtom (CAst.make @@ TacInductionDestruct(false, false, cl)) in
match EConstr.kind sigma t with
- | Case (_,_,_,x,_) when closed0 sigma x ->
+ | Case (_,_,_,_,_,x,_) when closed0 sigma x ->
if isVar sigma x then
(* TODO check there is no rel n. *)
raise (Found (Tacinterp.eval_tactic dest))
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 59533eb3e3..6d0e0c36b3 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -918,7 +918,8 @@ let reset_env env =
Environ.push_rel_context (Environ.rel_context env) env'
let fold_match ?(force=false) env sigma c =
- let (ci, p, iv, c, brs) = destCase sigma c in
+ let case = destCase sigma c in
+ let (ci, p, iv, c, brs) = EConstr.expand_case env sigma case in
let cty = Retyping.get_type_of env sigma c in
let dep, pred, exists, sk =
let env', ctx, body =
@@ -986,7 +987,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
let argty = Retyping.get_type_of env (goalevars evars) arg in
let state, res = s.strategy { state ; env ;
unfresh ;
- term1 = arg ; ty1 = argty ;
+ term1 = arg ; ty1 = argty ;
cstr = (prop,None) ;
evars } in
let res' =
@@ -1153,7 +1154,8 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
| Fail | Identity -> b'
in state, res
- | Case (ci, p, iv, c, brs) ->
+ | Case (ci, u, pms, p, iv, c, brs) ->
+ let (ci, p, iv, c, brs) = EConstr.expand_case env (goalevars evars) (ci, u, pms, p, iv, c, brs) in
let cty = Retyping.get_type_of env (goalevars evars) c in
let evars', eqty = app_poly_sort prop env evars coq_eq [| cty |] in
let cstr' = Some eqty in
@@ -1163,7 +1165,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
let state, res =
match c' with
| Success r ->
- let case = mkCase (ci, lift 1 p, map_invert (lift 1) iv, mkRel 1, Array.map (lift 1) brs) in
+ let case = mkCase (EConstr.contract_case env (goalevars evars) (ci, lift 1 p, map_invert (lift 1) iv, mkRel 1, Array.map (lift 1) brs)) in
let res = make_leibniz_proof env case ty r in
state, Success (coerce env (prop,cstr) res)
| Fail | Identity ->
@@ -1185,7 +1187,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
in
match found with
| Some r ->
- let ctxc = mkCase (ci, lift 1 p, map_invert (lift 1) iv, lift 1 c, Array.of_list (List.rev (brs' c'))) in
+ let ctxc = mkCase (EConstr.contract_case env (goalevars evars) (ci, lift 1 p, map_invert (lift 1) iv, lift 1 c, Array.of_list (List.rev (brs' c')))) in
state, Success (make_leibniz_proof env ctxc ty r)
| None -> state, c'
else
@@ -1386,7 +1388,7 @@ module Strategies =
let fold_glob c : 'a pure_strategy = { strategy =
fun { state ; env ; term1 = t ; ty1 = ty ; cstr ; evars } ->
-(* let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
+(* let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
let sigma, c = Pretyping.understand_tcc env (goalevars evars) c in
let unfolded =
try Tacred.try_red_product env sigma c
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 2a21049c6e..7774258fca 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -285,7 +285,8 @@ let iter_constr_LR f c = match kind c with
| Prod (_, t, b) | Lambda (_, t, b) -> f t; f b
| LetIn (_, v, t, b) -> f v; f t; f b
| App (cf, a) -> f cf; Array.iter f a
- | Case (_, p, iv, v, b) -> f v; iter_invert f iv; f p; Array.iter f b
+ | Case (_, _, pms, (_, p), iv, v, b) ->
+ f v; Array.iter f pms; f p; iter_invert f iv; Array.iter (fun (_, c) -> f c) b
| 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
@@ -749,7 +750,7 @@ let rec uniquize = function
EConstr.push_rel ctx_item env, h' + 1 in
let self acc c = EConstr.of_constr (subst_loop acc (EConstr.Unsafe.to_constr c)) in
let f = EConstr.of_constr f in
- let f' = map_constr_with_binders_left_to_right sigma inc_h self acc f in
+ let f' = map_constr_with_binders_left_to_right env sigma inc_h self acc f in
let f' = EConstr.Unsafe.to_constr f' in
mkApp (f', Array.map_left (subst_loop acc) a) in
subst_loop (env,h) c) : find_P),
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:35:27 +0000