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 /proofs/clenv.ml | |
| parent | b017e302f69f20fc4fc3d4088a305194f6c387fa (diff) | |
UIP in SProp
Diffstat (limited to 'proofs/clenv.ml')
| -rw-r--r-- | proofs/clenv.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 7fb3a21813..4d148756b4 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -263,7 +263,7 @@ let meta_reducible_instance env evd b = let rec irec u = let u = whd_betaiota env Evd.empty u (* FIXME *) in match EConstr.kind evd u with - | Case (ci,p,c,bl) when EConstr.isMeta evd (strip_outer_cast evd c) -> + | Case (ci,p,iv,c,bl) when EConstr.isMeta evd (strip_outer_cast evd c) -> let m = destMeta evd (strip_outer_cast evd c) in (match try @@ -272,8 +272,8 @@ let meta_reducible_instance env evd b = if isConstruct evd g || not is_coerce then Some g else None with Not_found -> None with - | Some g -> irec (mkCase (ci,p,g,bl)) - | None -> mkCase (ci,irec p,c,Array.map irec bl)) + | Some g -> irec (mkCase (ci,p,iv,g,bl)) + | None -> mkCase (ci,irec p,iv,c,Array.map irec bl)) | App (f,l) when EConstr.isMeta evd (strip_outer_cast evd f) -> let m = destMeta evd (strip_outer_cast evd f) in (match @@ -621,8 +621,8 @@ let clenv_cast_meta clenv = else mkCast (mkMeta mv, DEFAULTcast, b) with Not_found -> u) | App(f,args) -> mkApp (crec_hd f, Array.map crec args) - | Case(ci,p,c,br) -> - mkCase (ci, crec_hd p, crec_hd c, Array.map crec br) + | Case(ci,p,iv,c,br) -> + mkCase (ci, crec_hd p, map_invert crec_hd iv, crec_hd c, Array.map crec br) | Proj (p, c) -> mkProj (p, crec_hd c) | _ -> u in |