diff options
| author | Pierre-Marie Pédrot | 2016-11-25 18:34:53 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:30:41 +0100 |
| commit | 02dd160233adc784eac732d97a88356d1f0eaf9b (patch) | |
| tree | d2baacdc2a4ae06e4607bfe09b48ba2c23a78a0f /ltac/extraargs.ml4 | |
| parent | a5499688bd76def8de3d8e1089a49c7a08430903 (diff) | |
Removing various compatibility layers of tactics.
Diffstat (limited to 'ltac/extraargs.ml4')
| -rw-r--r-- | ltac/extraargs.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4 index f8db0b4fcd..53b726432c 100644 --- a/ltac/extraargs.ml4 +++ b/ltac/extraargs.ml4 @@ -177,7 +177,7 @@ ARGUMENT EXTEND lglob END let interp_casted_constr ist gl c = - interp_constr_gen (Pretyping.OfType (EConstr.of_constr (pf_concl gl))) ist (pf_env gl) (project gl) c + interp_constr_gen (Pretyping.OfType (pf_concl gl)) ist (pf_env gl) (project gl) c ARGUMENT EXTEND casted_constr TYPED AS constr |