diff options
Diffstat (limited to 'plugins/funind/functional_principles_proofs.ml')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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) |