diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-07 19:07:16 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:27:20 +0100 |
| commit | ce2b509734f3b70494a0a35b0b4eda593c1c8eb6 (patch) | |
| tree | 77e87e5da2b453e9ae918eef039b6511d3612597 /pretyping/classops.mli | |
| parent | 3b8acc174490878a3d0c9345e34a0ecb1d3abd66 (diff) | |
Classops API using EConstr.
Diffstat (limited to 'pretyping/classops.mli')
| -rw-r--r-- | pretyping/classops.mli | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/pretyping/classops.mli b/pretyping/classops.mli index d509739cf..4b8a2c1c0 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -59,15 +59,15 @@ val class_info_from_index : cl_index -> cl_typ * cl_info_typ (** [find_class_type env sigma c] returns the head reference of [c], its universe instance and its arguments *) -val find_class_type : evar_map -> types -> cl_typ * Univ.universe_instance * constr list +val find_class_type : evar_map -> EConstr.types -> cl_typ * Univ.universe_instance * constr list (** raises [Not_found] if not convertible to a class *) -val class_of : env -> evar_map -> types -> types * cl_index +val class_of : env -> evar_map -> EConstr.types -> types * cl_index (** raises [Not_found] if not mapped to a class *) val inductive_class_of : inductive -> cl_index -val class_args_of : env -> evar_map -> types -> constr list +val class_args_of : env -> evar_map -> EConstr.types -> constr list (** {6 [declare_coercion] adds a coercion in the graph of coercion paths } *) val declare_coercion : @@ -84,11 +84,11 @@ val coercion_value : coe_index -> (unsafe_judgment * bool * bool) Univ.in_univer (** @raise Not_found in the following functions when no path exists *) val lookup_path_between_class : cl_index * cl_index -> inheritance_path -val lookup_path_between : env -> evar_map -> types * types -> +val lookup_path_between : env -> evar_map -> EConstr.types * EConstr.types -> types * types * inheritance_path -val lookup_path_to_fun_from : env -> evar_map -> types -> +val lookup_path_to_fun_from : env -> evar_map -> EConstr.types -> types * inheritance_path -val lookup_path_to_sort_from : env -> evar_map -> types -> +val lookup_path_to_sort_from : env -> evar_map -> EConstr.types -> types * inheritance_path val lookup_pattern_path_between : env -> inductive * inductive -> (constructor * int) list |