diff options
Diffstat (limited to 'pretyping/pretyping.mli')
| -rw-r--r-- | pretyping/pretyping.mli | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 7395e94a0..5822f5add 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -18,7 +18,6 @@ open Evd open EConstr open Glob_term open Evarutil -open Misctypes (** An auxiliary function for searching for fixpoint guard indexes *) @@ -119,9 +118,6 @@ val ise_pretype_gen : (** To embed constr in glob_constr *) -val interp_sort : ?loc:Loc.t -> evar_map -> glob_sort -> evar_map * sorts -val interp_elimination_sort : glob_sort -> sorts_family - val register_constr_interp0 : ('r, 'g, 't) Genarg.genarg_type -> (unbound_ltac_var_map -> env -> evar_map -> types -> 'g -> constr * evar_map) -> unit |