Merge pull request #134 from SkySkimmer/no-vm

Don't use vmcast to convert the reified goal and actual goal

src/aac_rewrite.ml

@@ -135,7 +135,7 @@ let by_aac_reflexivity zero
   (* This convert is required to deal with evars in a proper
      way *)
   let convert_to = mkApp (r, [| mkApp (eval,[| t |]); mkApp (eval, [|t'|])|])   in
-  let convert = Tactics.convert_concl ~cast:true ~check:true convert_to Constr.VMcast in
+  let convert = Tactics.convert_concl ~cast:true ~check:true convert_to Constr.DEFAULTcast in
   let apply_tac = Tactics.apply decision_thm in
   let open Proofview in
   Coq.tclRETYPE decision_thm
@@ -167,7 +167,7 @@ let by_aac_normalise zero lift ir t t' =
   (* This convert is required to deal with evars in a proper
      way *)
   let convert_to = mkApp (rlt.Coq.Relation.r, [| mkApp (eval,[| t |]); mkApp (eval, [|t'|])|])   in
-  let convert = Tactics.convert_concl ~cast:true ~check:true convert_to Constr.VMcast in
+  let convert = Tactics.convert_concl ~cast:true ~check:true convert_to Constr.DEFAULTcast in
   let apply_tac = Tactics.apply normalise_thm in
   Tacticals.tclTHENLIST
     [ Coq.tclRETYPE normalise_thm; Coq.tclRETYPE convert_to;