diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-02 10:06:21 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-02 10:06:21 +0000 |
| commit | 307c7610df6389768848e574170da85f1ab2c8fe (patch) | |
| tree | 656e753eb1fd5c1863385b0d27b552ed7643ca10 /pretyping/classops.mli | |
| parent | 653f63e8b49fd46e686619d8e847e571d8c5442a (diff) | |
Propagating commit 11343 from branch v8.2 to trunk (wish 1934 about
backtracking on coercion classes when a coercion path fails).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11344 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/classops.mli')
| -rw-r--r-- | pretyping/classops.mli | 23 |
1 files changed, 14 insertions, 9 deletions
diff --git a/pretyping/classops.mli b/pretyping/classops.mli index c1a62b34f..a5f139ab1 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -52,17 +52,17 @@ val class_info : cl_typ -> (cl_index * cl_info_typ) val class_exists : cl_typ -> bool val class_info_from_index : cl_index -> cl_typ * cl_info_typ -(* [find_class_type c] returns the head reference of c and its +(* [find_class_type env sigma c] returns the head reference of [c] and its arguments *) -val find_class_type : constr -> cl_typ * constr list +val find_class_type : env -> evar_map -> types -> cl_typ * constr list (* raises [Not_found] if not convertible to a class *) -val class_of : env -> evar_map -> constr -> constr * cl_index +val class_of : env -> evar_map -> types -> types * cl_index (* raises [Not_found] if not mapped to a class *) val inductive_class_of : inductive -> cl_index -val class_args_of : constr -> constr list +val class_args_of : env -> evar_map -> types -> constr list (*s [declare_coercion] adds a coercion in the graph of coercion paths *) val declare_coercion : @@ -75,11 +75,16 @@ val coercion_exists : coe_typ -> bool val coercion_value : coe_index -> (unsafe_judgment * bool) (*s Lookup functions for coercion paths *) -val lookup_path_between : cl_index * cl_index -> inheritance_path -val lookup_path_to_fun_from : cl_index -> inheritance_path -val lookup_path_to_sort_from : cl_index -> inheritance_path -val lookup_pattern_path_between : - cl_index * cl_index -> (constructor * int) list +val lookup_path_between_class : cl_index * cl_index -> inheritance_path + +val lookup_path_between : env -> evar_map -> types * types -> + types * types * inheritance_path +val lookup_path_to_fun_from : env -> evar_map -> types -> + types * inheritance_path +val lookup_path_to_sort_from : env -> evar_map -> types -> + types * inheritance_path +val lookup_pattern_path_between : + inductive * inductive -> (constructor * int) list (*i Crade *) open Pp |