diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-27 19:27:52 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-27 19:39:43 +0100 |
| commit | 1ec0928ebecc8fa51022b681d32665d4f010e0ef (patch) | |
| tree | 405ebadc827fc916f0a356884c53ec708846447c /tactics/tacinterp.mli | |
| parent | cbd815a289db52f58235f23f5afba3be49cc8eed (diff) | |
Factorizing code for untyped constr evaluation.
Diffstat (limited to 'tactics/tacinterp.mli')
| -rw-r--r-- | tactics/tacinterp.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index c67aa31a9..5b81da74a 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -65,6 +65,11 @@ val val_interp : interp_sign -> glob_tactic_expr -> (value -> unit Proofview.tac (** Interprets an expression that evaluates to a constr *) val interp_ltac_constr : interp_sign -> glob_tactic_expr -> (constr -> unit Proofview.tactic) -> unit Proofview.tactic +val type_uconstr : + ?flags:Pretyping.inference_flags -> + ?expected_type:Pretyping.typing_constraint -> + interp_sign -> Glob_term.closed_glob_constr -> constr delayed_open + (** Interprets redexp arguments *) val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map * red_expr |