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/ltac/rewrite.ml | |
| parent | b017e302f69f20fc4fc3d4088a305194f6c387fa (diff) | |
UIP in SProp
Diffstat (limited to 'plugins/ltac/rewrite.ml')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 40dea90c00..fb149071c9 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -923,8 +923,8 @@ let reset_env env = let env' = Global.env_of_context (Environ.named_context_val env) in Environ.push_rel_context (Environ.rel_context env) env' -let fold_match env sigma c = - let (ci, p, c, brs) = destCase sigma c in +let fold_match ?(force=false) env sigma c = + let (ci, p, iv, c, brs) = destCase sigma c in let cty = Retyping.get_type_of env sigma c in let dep, pred, exists, sk = let env', ctx, body = @@ -1184,7 +1184,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = | Fail | Identity -> b' in state, res - | Case (ci, p, c, brs) -> + | Case (ci, p, iv, c, brs) -> let cty = Retyping.get_type_of env (goalevars evars) c in let evars', eqty = app_poly_sort prop env evars coq_eq [| cty |] in let cstr' = Some eqty in @@ -1194,7 +1194,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = let state, res = match c' with | Success r -> - let case = mkCase (ci, lift 1 p, mkRel 1, Array.map (lift 1) brs) in + let case = mkCase (ci, lift 1 p, map_invert (lift 1) iv, mkRel 1, Array.map (lift 1) brs) in let res = make_leibniz_proof env case ty r in state, Success (coerce env unfresh (prop,cstr) res) | Fail | Identity -> @@ -1216,7 +1216,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = in match found with | Some r -> - let ctxc = mkCase (ci, lift 1 p, lift 1 c, Array.of_list (List.rev (brs' c'))) in + let ctxc = mkCase (ci, lift 1 p, map_invert (lift 1) iv, lift 1 c, Array.of_list (List.rev (brs' c'))) in state, Success (make_leibniz_proof env ctxc ty r) | None -> state, c' else |