diff options
| -rw-r--r-- | proofs/logic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 071e44b5be..59ff7a3224 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -627,7 +627,7 @@ let prim_extractor subfun vl pft = (* Structural and conversion rules do not produce any proof *) | Some (Prim (Convert_concl (t,k)),[pf]) -> if k = DEFAULTcast then subfun vl pf - else mkCast (subfun vl pf,k,cl) + else mkCast (subfun vl pf,k,subst_proof_vars vl cl) | Some (Prim (Convert_hyp _),[pf]) -> subfun vl pf |