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

VM can't avoid computing subterms of the goal that should be left alone.

Fix #133

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