diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
| commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
| tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /contrib/subtac/subtac_command.mli | |
| parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) | |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'contrib/subtac/subtac_command.mli')
| -rw-r--r-- | contrib/subtac/subtac_command.mli | 50 |
1 files changed, 0 insertions, 50 deletions
diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli deleted file mode 100644 index 3a6a351b..00000000 --- a/contrib/subtac/subtac_command.mli +++ /dev/null @@ -1,50 +0,0 @@ -open Pretyping -open Evd -open Environ -open Term -open Topconstr -open Names -open Libnames -open Pp -open Vernacexpr -open Constrintern - -val interp_gen : - typing_constraint -> - evar_defs ref -> - env -> - ?impls:full_implicits_env -> - ?allow_patvar:bool -> - ?ltacvars:ltac_sign -> - constr_expr -> constr -val interp_constr : - evar_defs ref -> - env -> constr_expr -> constr -val interp_type_evars : - evar_defs ref -> - env -> - ?impls:full_implicits_env -> - constr_expr -> constr -val interp_casted_constr_evars : - evar_defs ref -> - env -> - ?impls:full_implicits_env -> - constr_expr -> types -> constr -val interp_open_constr : - evar_defs ref -> env -> constr_expr -> constr -val interp_constr_judgment : - evar_defs ref -> - env -> - constr_expr -> unsafe_judgment -val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list - -val interp_binder : Evd.evar_defs ref -> - Environ.env -> Names.name -> Topconstr.constr_expr -> Term.constr - - - -val build_recursive : - (fixpoint_expr * decl_notation) list -> bool -> unit - -val build_corecursive : - (cofixpoint_expr * decl_notation) list -> bool -> unit |