diff options
Diffstat (limited to 'ltac/extraargs.ml4')
| -rw-r--r-- | ltac/extraargs.ml4 | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4 index 0bddcc9fd..9a2a176cb 100644 --- a/ltac/extraargs.ml4 +++ b/ltac/extraargs.ml4 @@ -15,6 +15,7 @@ open Constrarg open Pcoq.Prim open Pcoq.Constr open Names +open Tacmach open Tacexpr open Taccoerce open Tacinterp @@ -175,6 +176,16 @@ ARGUMENT EXTEND lglob [ lconstr(c) ] -> [ c ] END +let interp_casted_constr ist gl c = + interp_constr_gen (Pretyping.OfType (pf_concl gl)) ist (pf_env gl) (project gl) c + +ARGUMENT EXTEND casted_constr + TYPED AS constr + PRINTED BY pr_gen + INTERPRETED BY interp_casted_constr + [ constr(c) ] -> [ c ] +END + type 'id gen_place= ('id * hyp_location_flag,unit) location type loc_place = Id.t Loc.located gen_place |