diff options
Diffstat (limited to 'ltac/extratactics.ml4')
| -rw-r--r-- | ltac/extratactics.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index c3ca8f906..3e7cf5d13 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -734,7 +734,7 @@ let refl_equal = call it before it is defined. *) let mkCaseEq a : unit Proofview.tactic = Proofview.Goal.nf_enter { enter = begin fun gl -> - let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g a) gl in + let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g (EConstr.of_constr a)) gl in Tacticals.New.tclTHENLIST [Tactics.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]; Proofview.Goal.nf_enter { enter = begin fun gl -> @@ -789,7 +789,7 @@ let destauto t = let destauto_in id = Proofview.Goal.nf_enter { enter = begin fun gl -> - let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g (mkVar id)) gl in + let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g (EConstr.mkVar id)) gl in (* Pp.msgnl (Printer.pr_lconstr (mkVar id)); *) (* Pp.msgnl (Printer.pr_lconstr (ctype)); *) destauto ctype |