Tacred API using EConstr.

1 files changed, 2 insertions, 2 deletions

diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index ca1f6e6385..e1b4681975 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -300,7 +300,7 @@ let project_hint pri l2r r =
   let sigma, c = Evd.fresh_global env sigma gr in
   let t = Retyping.get_type_of env sigma (EConstr.of_constr c) in
   let t =
-    Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) t in
+    Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) (EConstr.of_constr t) in
   let sign,ccl = decompose_prod_assum t in
   let (a,b) = match snd (decompose_app ccl) with
     | [a;b] -> (a,b)
@@ -738,7 +738,7 @@ let  mkCaseEq a  : unit Proofview.tactic =
             let concl = Proofview.Goal.concl gl in
             let env = Proofview.Goal.env gl in
             (** FIXME: this looks really wrong. Does anybody really use this tactic? *)
-            let Sigma (c, _, _) = (Tacred.pattern_occs [Locus.OnlyOccurrences [1], a]).Reductionops.e_redfun env (Sigma.Unsafe.of_evar_map Evd.empty) (EConstr.of_constr concl) in
+            let Sigma (c, _, _) = (Tacred.pattern_occs [Locus.OnlyOccurrences [1], EConstr.of_constr a]).Reductionops.e_redfun env (Sigma.Unsafe.of_evar_map Evd.empty) (EConstr.of_constr concl) in
 	    change_concl c
           end };
 	  simplest_case a]