diff options
| -rw-r--r-- | tactics/autorewrite.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 469fc5e42c..29ae191b39 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -153,7 +153,7 @@ let subst_hintrewrite (_,subst,(rbase,list as node)) = typ (* dummy value, it will be recomputed by cache_hintrewrite *) in let t' = Tacinterp.subst_tactic subst t in if cst == cst' && t == t' then pair else - (cst',typ',b,t) + (cst',typ',b,t') in let list' = list_smartmap subst_first list in if list' == list then node else |