diff options
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 f8db0b4fc..53b726432 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 |