aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml6
-rw-r--r--plugins/funind/g_indfun.mlg25
-rw-r--r--plugins/funind/gen_principle.ml14
-rw-r--r--plugins/funind/indfun_common.ml1
-rw-r--r--plugins/funind/indfun_common.mli2
-rw-r--r--plugins/funind/recdef.ml12
6 files changed, 38 insertions, 22 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 73eb943418..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)
@@ -1260,7 +1260,7 @@ let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num
tclTHENLIST
[ unfold_in_concl
[ ( Locus.AllOccurrences
- , Names.EvalConstRef (fst fname) ) ]
+ , Tacred.EvalConstRef (fst fname) ) ]
; (let do_prove =
build_proof interactive_proof
(Array.to_list fnames)
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index ca6ae150a7..15cf88f827 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -195,16 +195,29 @@ let is_interactive recsl =
}
+(* For usability we temporarily switch off some flags during the call
+ to Function. However this is not satisfactory:
+
+ 1- Function should not warn "non-recursive" and call the Definition
+ mechanism instead of Fixpoint when needed
+
+ 2- Only for automatically generated names should
+ unused-pattern-matching-variable be ignored. *)
+
VERNAC COMMAND EXTEND Function STATE CUSTOM
| ["Function" ne_function_fix_definition_list_sep(recsl,"with")]
=> { classify_funind recsl }
-> {
- if is_interactive recsl then
- Vernacextend.VtOpenProof (fun () ->
- Gen_principle.do_generate_principle_interactive (List.map snd recsl))
- else
- Vernacextend.VtDefault (fun () ->
- Gen_principle.do_generate_principle (List.map snd recsl)) }
+ let warn = "-unused-pattern-matching-variable,-matching-variable,-non-recursive" in
+ if is_interactive recsl then
+ Vernacextend.VtOpenProof (fun () ->
+ CWarnings.with_warn warn
+ Gen_principle.do_generate_principle_interactive (List.map snd recsl))
+ else
+ Vernacextend.VtDefault (fun () ->
+ CWarnings.with_warn warn
+ Gen_principle.do_generate_principle (List.map snd recsl))
+ }
END
{
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 314c8abcaf..cbdebb7bbc 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -917,13 +917,13 @@ and intros_with_rewrite_aux () : unit Proofview.tactic =
tclTHENLIST
[ unfold_in_concl
[ ( Locus.AllOccurrences
- , Names.EvalVarRef (destVar sigma args.(1)) ) ]
+ , Tacred.EvalVarRef (destVar sigma args.(1)) ) ]
; tclMAP
(fun id ->
tclTRY
(unfold_in_hyp
[ ( Locus.AllOccurrences
- , Names.EvalVarRef (destVar sigma args.(1)) ) ]
+ , Tacred.EvalVarRef (destVar sigma args.(1)) ) ]
(destVar sigma args.(1), Locus.InHyp)))
(pf_ids_of_hyps g)
; intros_with_rewrite () ]
@@ -936,13 +936,13 @@ and intros_with_rewrite_aux () : unit Proofview.tactic =
tclTHENLIST
[ unfold_in_concl
[ ( Locus.AllOccurrences
- , Names.EvalVarRef (destVar sigma args.(2)) ) ]
+ , Tacred.EvalVarRef (destVar sigma args.(2)) ) ]
; tclMAP
(fun id ->
tclTRY
(unfold_in_hyp
[ ( Locus.AllOccurrences
- , Names.EvalVarRef (destVar sigma args.(2)) ) ]
+ , Tacred.EvalVarRef (destVar sigma args.(2)) ) ]
(destVar sigma args.(2), Locus.InHyp)))
(pf_ids_of_hyps g)
; intros_with_rewrite () ]
@@ -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
@@ -1158,7 +1158,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i :
else
unfold_in_concl
[ ( Locus.AllOccurrences
- , Names.EvalConstRef
+ , Tacred.EvalConstRef
(fst (destConst (Proofview.Goal.sigma g) f)) ) ]
in
(* The proof of each branche itself *)
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 6464556e4e..266345a324 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -418,6 +418,7 @@ let make_eq () =
with _ -> assert false
let evaluable_of_global_reference r =
+ let open Tacred in
(* Tacred.evaluable_of_global_reference (Global.env ()) *)
match r with
| GlobRef.ConstRef sp -> EvalConstRef sp
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 7b7044fdaf..e25f413fe4 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -100,7 +100,7 @@ val acc_rel : EConstr.constr Util.delayed
val well_founded : EConstr.constr Util.delayed
val evaluable_of_global_reference :
- GlobRef.t -> Names.evaluable_global_reference
+ GlobRef.t -> Tacred.evaluable_global_reference
val list_rewrite : bool -> (EConstr.constr * bool) list -> unit Proofview.tactic
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 33076a876b..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, t, 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 01:13:15 +0000