diff options
Diffstat (limited to 'tactics/setoid_replace.ml')
| -rw-r--r-- | tactics/setoid_replace.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 644a68666a..22596ac3c0 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -1815,7 +1815,7 @@ let relation_rewrite c1 c2 (input_direction,cl) ~new_goals gl = let analyse_hypothesis gl c = let ctype = pf_type_of gl c in let eqclause = Clenv.make_clenv_binding gl (c,ctype) Rawterm.NoBindings in - let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in + let (equiv, args) = decompose_app (Clenv.clenv_direct_nf_type eqclause) in let rec split_last_two = function | [c1;c2] -> [],(c1, c2) | x::y::z -> |