Bug fixed: rewrite > t where t had occurrences of metavariables in it could

fail because of a missing apply_subst.

diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml
index da7f599a9ec2b642291173c3d0c6c1d4a6fc5bf6..cca2c1a5902b9256736dd8b1001abe42c1d3ea22 100644 (file)
--- a/helm/software/components/tactics/equalityTactics.ml
+++ b/helm/software/components/tactics/equalityTactics.ml
@@ -145,6 +145,7 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit
     selected_terms_with_context ([],[]) in
   let t1 = CicMetaSubst.apply_subst subst t1 in
   let t2 = CicMetaSubst.apply_subst subst t2 in
+  let ty = CicMetaSubst.apply_subst subst ty in
   let equality = CicMetaSubst.apply_subst subst equality in
   let abstr_gty =
    ProofEngineReduction.replace_lifting_csc 0