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 /kernel/inductive.ml | |
| parent | b017e302f69f20fc4fc3d4088a305194f6c387fa (diff) | |
UIP in SProp
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 8423813639..c51d82ce07 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -756,7 +756,7 @@ let rec subterm_specif renv stack t = let f,l = decompose_app (whd_all renv.env t) in match kind f with | Rel k -> subterm_var k renv - | Case (ci,p,c,lbr) -> + | Case (ci,p,_iv,c,lbr) -> (* iv ignored: it's just a cache *) let stack' = push_stack_closures renv l stack in let cases_spec = branches_specif renv (lazy_subterm_specif renv [] c) ci @@ -954,7 +954,7 @@ let check_one_fix renv recpos trees def = check_rec_call renv stack (Term.applist(lift p c,l)) end - | Case (ci,p,c_0,lrest) -> + | Case (ci,p,iv,c_0,lrest) -> (* iv ignored: it's just a cache *) begin try List.iter (check_rec_call renv []) (c_0::p::l); (* compute the recarg info for the arguments of each branch *) @@ -976,7 +976,7 @@ let check_one_fix renv recpos trees def = (* the call to whd_betaiotazeta will reduce the apparent iota redex away *) check_rec_call renv [] - (Term.applist (mkCase (ci,p,c_0,lrest), l)) + (Term.applist (mkCase (ci,p,iv,c_0,lrest), l)) | _ -> Exninfo.iraise exn end @@ -1254,7 +1254,7 @@ let check_one_cofix env nbfix def deftype = else raise (CoFixGuardError (env,UnguardedRecursiveCall c)) - | Case (_,p,tm,vrest) -> + | Case (_,p,_,tm,vrest) -> (* iv ignored: just a cache *) begin let tree = match restrict_spec env (Subterm (Strict, tree)) p with | Dead_code -> assert false |