diff options
| author | Pierre-Marie Pédrot | 2016-11-06 21:59:18 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:26:38 +0100 |
| commit | b77579ac873975a15978c5a4ecf312d577746d26 (patch) | |
| tree | 772e41667e74c38582ff6f4645c73e7d7556f935 /ltac | |
| parent | 258c8502eafd3e078a5c7478a452432b5c046f71 (diff) | |
Tacred API using EConstr.
Diffstat (limited to 'ltac')
| -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 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] |