diff options
| author | Gaëtan Gilbert | 2019-06-13 15:39:43 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-01 13:06:22 +0200 |
| commit | 2ded4c25e532c5dfca0483c211653768ebed01a7 (patch) | |
| tree | a04b2f787490c8971590e6bdf7dd1ec4220e0290 /plugins/funind/functional_principles_proofs.ml | |
| parent | b017e302f69f20fc4fc3d4088a305194f6c387fa (diff) | |
UIP in SProp
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 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 |