diff options
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/extratactics.ml4 | 4 | ||||
| -rw-r--r-- | ltac/rewrite.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index c3ca8f906f..3e7cf5d13b 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 diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index dfcfbfbd35..37b9a9edbc 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -2188,7 +2188,7 @@ let setoid_transitivity c = let setoid_symmetry_in id = Proofview.V82.tactic (fun gl -> - let ctype = pf_unsafe_type_of gl (mkVar id) in + let ctype = pf_unsafe_type_of gl (EConstr.mkVar id) in let binders,concl = decompose_prod_assum ctype in let (equiv, args) = decompose_app concl in let rec split_last_two = function |