diff options
| author | Maxime Dénès | 2017-06-06 08:56:35 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-06 08:56:35 +0200 |
| commit | 98dc4f985f2ddd47b4d4d6afee901a0a2bb0bde0 (patch) | |
| tree | 9b8958585f6e593874f2deb789b2f01fb237637c /plugins/ltac/tacinterp.mli | |
| parent | 6e4d1ee9bb61601df041fe44eb60b4fa059080d5 (diff) | |
| parent | a07c0579a2d4b660b3b9996cd79bdf8e0f588949 (diff) | |
Merge PR#600: Some factorizations of ltac interpretation functions between ssreflect and coq code
Diffstat (limited to 'plugins/ltac/tacinterp.mli')
| -rw-r--r-- | plugins/ltac/tacinterp.mli | 18 |
1 files changed, 17 insertions, 1 deletions
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index 2ec45312ea..fb50a64346 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -72,11 +72,27 @@ val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map val interp_hyp : interp_sign -> Environ.env -> Evd.evar_map -> Id.t Loc.located -> Id.t +val interp_glob_closure : interp_sign -> Environ.env -> Evd.evar_map -> + ?kind:Pretyping.typing_constraint -> ?pattern_mode:bool -> glob_constr_and_expr -> + Glob_term.closed_glob_constr + +val interp_uconstr : interp_sign -> Environ.env -> Evd.evar_map -> + glob_constr_and_expr -> Glob_term.closed_glob_constr + val interp_constr_gen : Pretyping.typing_constraint -> interp_sign -> Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Evd.evar_map * constr val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map -> - glob_constr_and_expr bindings -> Evd.evar_map * constr bindings + glob_constr_and_expr bindings -> Evd.evar_map * constr bindings + +val interp_open_constr : ?expected_type:Pretyping.typing_constraint -> + ?flags:Pretyping.inference_flags -> + interp_sign -> Environ.env -> Evd.evar_map -> + glob_constr_and_expr -> Evd.evar_map * EConstr.constr + +val interp_open_constr_with_classes : ?expected_type:Pretyping.typing_constraint -> + interp_sign -> Environ.env -> Evd.evar_map -> + glob_constr_and_expr -> Evd.evar_map * EConstr.constr val interp_open_constr_with_bindings : interp_sign -> Environ.env -> Evd.evar_map -> glob_constr_and_expr with_bindings -> Evd.evar_map * EConstr.constr with_bindings |