aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/btauto/refl_btauto.ml2
-rw-r--r--plugins/extraction/extraction.ml15
-rw-r--r--plugins/firstorder/unify.ml8
-rw-r--r--plugins/funind/functional_principles_proofs.ml4
-rw-r--r--plugins/funind/gen_principle.ml4
-rw-r--r--plugins/funind/recdef.ml23
-rw-r--r--plugins/ltac/extratactics.mlg2
-rw-r--r--plugins/ltac/rewrite.ml10
-rw-r--r--plugins/setoid_ring/newring.ml2
-rw-r--r--plugins/ssrmatching/ssrmatching.ml2
10 files changed, 40 insertions, 32 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 52c6c5d0f9..23f8fe04a3 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -112,7 +112,7 @@ 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, arg, pats) ->
+ | Case (info, r, _iv, arg, pats) ->
let is_bool =
let i = info.ci_ind in
Names.eq_ind i (Lazy.force ind)
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 0f96b9bbe8..a7c926f50c 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -291,7 +291,7 @@ let rec extract_type env sg db j c args =
let reason = if lvl == TypeScheme then Ktype else Kprop in
Tarr (Tdummy reason, mld)))
| Sort _ -> Tdummy Ktype (* The two logical cases. *)
- | _ when sort_of env sg (applistc c args) == InProp -> Tdummy Kprop
+ | _ when info_of_family (sort_of env sg (applistc c args)) == Logic -> Tdummy Kprop
| Rel n ->
(match EConstr.lookup_rel n env with
| LocalDef (_,t,_) ->
@@ -672,8 +672,9 @@ 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},_,c0,br) ->
- extract_app env sg mle mlt (extract_case env sg mle (ip,c0,br)) 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
| Fix ((_,i),recd) ->
extract_app env sg mle mlt (extract_fix env sg mle i recd) args
| CoFix (i,recd) ->
@@ -852,8 +853,8 @@ and extract_case env sg mle ((kn,i) as ip,c,br) mlt =
end else
(* [c] has an inductive type, and is not a type scheme type. *)
let t = type_of env sg c in
- (* The only non-informative case: [c] is of sort [Prop] *)
- if (sort_of env sg t) == InProp then
+ (* The only non-informative case: [c] is of sort [Prop]/[SProp] *)
+ if info_of_family (sort_of env sg t) == Logic then
begin
add_recursors env kn; (* May have passed unseen if logical ... *)
(* Logical singleton case: *)
@@ -1016,7 +1017,7 @@ let extract_fixpoint env sg vkn (fi,ti,ci) =
(* for replacing recursive calls [Rel ..] by the corresponding [Const]: *)
let sub = List.rev_map EConstr.mkConst kns in
for i = 0 to n-1 do
- if sort_of env sg ti.(i) != InProp then
+ if info_of_family (sort_of env sg ti.(i)) != Logic then
try
let e,t = extract_std_constant env sg vkn.(i)
(EConstr.Vars.substl sub ci.(i)) ti.(i) in
@@ -1073,7 +1074,7 @@ let fake_match_projection env p =
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, mkRel 1, [|branch|]) in
+ let body = mkCase (ci, 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 9c3debe48f..c62bc73e41 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -67,10 +67,10 @@ 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 (_,pa,_,ca,va),Case (_,pb,_,cb,vb)->
+ 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 9b578d4697..f2658a395f 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -585,10 +585,10 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos
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
- | Case (ci, ct, t, cb) ->
+ | Case (ci, ct, iv, t, cb) ->
let do_finalize_t dyn_info' g =
let t = dyn_info'.info in
- let dyn_infos = {dyn_info' with info = mkCase (ci, ct, t, cb)} in
+ let dyn_infos = {dyn_info' with info = mkCase (ci, ct, iv, t, cb)} in
let g_nb_prod = nb_prod (project g) (pf_concl g) in
let g, type_of_term = tac_type_of g t in
let term_eq = make_refl_eq (Lazy.force refl_equal) type_of_term t in
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 167cf37026..d09609bf7a 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -987,7 +987,7 @@ and intros_with_rewrite_aux : Tacmach.tactic =
( UnivGen.constr_of_monomorphic_global
@@ Coqlib.lib_ref "core.False.type" )) ->
Proofview.V82.of_tactic tauto g
- | Case (_, _, v, _) ->
+ | Case (_, _, _, v, _) ->
tclTHENLIST
[Proofview.V82.of_tactic (simplest_case v); intros_with_rewrite]
g
@@ -1026,7 +1026,7 @@ let rec reflexivity_with_destruct_cases g =
match
EConstr.kind (project g) (snd (destApp (project g) (pf_concl g))).(2)
with
- | Case (_, _, v, _) ->
+ | Case (_, _, _, v, _) ->
tclTHENLIST
[ Proofview.V82.of_tactic (simplest_case v)
; Proofview.V82.of_tactic intros
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 884792cc15..701ea56c2a 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -312,7 +312,7 @@ let check_not_nested env sigma forbidden e =
| Const _ -> ()
| Ind _ -> ()
| Construct _ -> ()
- | Case (_, t, e, a) ->
+ | Case (_, t, _, e, a) ->
check_not_nested t;
check_not_nested e;
Array.iter check_not_nested a
@@ -374,7 +374,13 @@ type journey_info =
; lambdA : (Name.t * types * constr, constr) journey_info_tac
; casE :
((constr infos -> tactic) -> constr infos -> tactic)
- -> (case_info * constr * constr * constr array, constr) journey_info_tac
+ -> ( case_info
+ * constr
+ * (constr, EInstance.t) case_invert
+ * constr
+ * constr array
+ , constr )
+ journey_info_tac
; otherS : (unit, constr) journey_info_tac
; apP : (constr * constr list, constr) journey_info_tac
; app_reC : (constr * constr list, constr) journey_info_tac
@@ -474,9 +480,9 @@ let rec travel_aux jinfo continuation_tac (expr_info : constr infos) g =
++ 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, a, l) ->
+ | Case (ci, t, iv, a, l) ->
let continuation_tac_a =
- jinfo.casE (travel jinfo) (ci, t, a, l) expr_info continuation_tac
+ jinfo.casE (travel jinfo) (ci, t, iv, a, l) expr_info continuation_tac
in
travel jinfo continuation_tac_a
{expr_info with info = a; is_main_branch = false; is_final = false}
@@ -767,7 +773,8 @@ let mkDestructEq not_on_hyp expr g =
in
(g, tac, to_revert)
-let terminate_case next_step (ci, a, t, l) expr_info continuation_tac infos g =
+let terminate_case next_step (ci, a, iv, t, l) expr_info continuation_tac infos
+ g =
let sigma = project g in
let env = pf_env g in
let f_is_present =
@@ -779,7 +786,7 @@ let terminate_case next_step (ci, a, t, l) expr_info continuation_tac infos g =
let a' = infos.info in
let new_info =
{ infos with
- info = mkCase (ci, t, a', l)
+ info = mkCase (ci, t, iv, a', l)
; is_main_branch = expr_info.is_main_branch
; is_final = expr_info.is_final }
in
@@ -916,10 +923,10 @@ let prove_terminate = travel terminate_info
(* Equation proof *)
-let equation_case next_step (ci, a, t, l) expr_info continuation_tac infos =
+let equation_case next_step case expr_info continuation_tac infos =
observe_tac
(fun _ _ -> str "equation case")
- (terminate_case next_step (ci, a, t, l) expr_info continuation_tac infos)
+ (terminate_case next_step case expr_info continuation_tac infos)
let rec prove_le g =
let sigma = project g in
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 40c64a1c26..66c72a30a2 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -776,7 +776,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 40dea90c00..fb149071c9 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -923,8 +923,8 @@ let reset_env env =
let env' = Global.env_of_context (Environ.named_context_val env) in
Environ.push_rel_context (Environ.rel_context env) env'
-let fold_match env sigma c =
- let (ci, p, c, brs) = destCase sigma c in
+let fold_match ?(force=false) env sigma c =
+ let (ci, p, iv, c, brs) = destCase sigma c in
let cty = Retyping.get_type_of env sigma c in
let dep, pred, exists, sk =
let env', ctx, body =
@@ -1184,7 +1184,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
| Fail | Identity -> b'
in state, res
- | Case (ci, p, c, brs) ->
+ | Case (ci, p, iv, c, brs) ->
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
@@ -1194,7 +1194,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, mkRel 1, Array.map (lift 1) brs) in
+ let case = mkCase (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 unfresh (prop,cstr) res)
| Fail | Identity ->
@@ -1216,7 +1216,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, lift 1 c, Array.of_list (List.rev (brs' c'))) in
+ let ctxc = mkCase (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
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 878f7a834e..95faede7d0 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -77,7 +77,7 @@ let protect_red map env sigma c0 =
let evars ev = Evarutil.safe_evar_value sigma ev in
let c = EConstr.Unsafe.to_constr c0 in
let tab = create_tab () in
- let infos = create_clos_infos ~evars all env in
+ let infos = create_clos_infos ~univs:(Evd.universes sigma) ~evars all env in
let map = lookup_map map sigma c0 in
let rec eval n c = match Constr.kind c with
| Prod (na, t, u) -> Constr.mkProd (na, eval n t, eval (n + 1) u)
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 5d6e7c51d0..162013c556 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -308,7 +308,7 @@ 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, v, b) -> f v; f p; Array.iter f b
+ | Case (_, p, iv, v, b) -> f v; iter_invert f iv; f p; Array.iter f 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:49:44 +0000