diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 4 | ||||
| -rw-r--r-- | tactics/rewrite.ml | 8 |
2 files changed, 8 insertions, 4 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 8eadd4aeec..6c550e9163 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -230,8 +230,8 @@ let rewrite_keyed_core_unif_flags = { (* This is set dynamically *) restrict_conv_on_strict_subterms = false; - modulo_betaiota = true; - (* Different from conv_closed *) + modulo_betaiota = false; + modulo_eta = true; } diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 8123bd755c..9532354632 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -484,11 +484,15 @@ let rec decompose_app_rel env evd t = let len = Array.length args in let fargs = Array.sub args 0 (Array.length args - 2) in let rel = mkApp (f, fargs) in - let ty = Retyping.get_type_of env evd rel in - let () = if not (Reduction.is_arity env ty) then error_no_relation () in rel, args.(len - 2), args.(len - 1) | _ -> error_no_relation () +let decompose_app_rel env evd t = + let (rel, t1, t2) = decompose_app_rel env evd t in + let ty = Retyping.get_type_of env evd rel in + let () = if not (Reduction.is_arity env ty) then error_no_relation () in + (rel, t1, t2) + let decompose_applied_relation env sigma (c,l) = let open Context.Rel.Declaration in let ctype = Retyping.get_type_of env sigma c in |