diff options
| author | Pierre-Marie Pédrot | 2016-11-11 19:52:48 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:28:44 +0100 |
| commit | cbea91d815f134d63d02d8fb1bd78ed97db28cd1 (patch) | |
| tree | adeb71808e2f4d6be1686071e79e96cf6761f3c0 /ltac/extratactics.ml4 | |
| parent | 53fe23265daafd47e759e73e8f97361c7fdd331b (diff) | |
Tacmach API using EConstr.
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 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 |