diff options
| -rw-r--r-- | pretyping/class.ml | 2 | ||||
| -rwxr-xr-x | pretyping/classops.ml | 8 |
2 files changed, 6 insertions, 4 deletions
diff --git a/pretyping/class.ml b/pretyping/class.ml index db67ac2be4..419bd1bf38 100644 --- a/pretyping/class.ml +++ b/pretyping/class.ml @@ -53,7 +53,7 @@ let rec stre_unif_cond = function stre_max (stre1,stre2) let stre_of_coe = function - | NAM_Constant sp -> constant_strength sp + | NAM_Constant sp -> constant_or_parameter_strength sp | NAM_Var id -> variable_strength id | NAM_Inductive _ | NAM_Constructor _ -> NeverDischarge diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 5f2557f1cb..230c2cb846 100755 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -169,7 +169,7 @@ let lookup_path_to_sort_from s = let (inClass,outClass) = declare_object ("CLASS", - { load_function = (fun _ -> ()); + { load_function = (function (_,x) -> add_new_class1 x); open_function = (fun _ -> ()); cache_function = (function (_,x) -> add_new_class1 x); specification_function = (function x -> x) }) @@ -239,7 +239,8 @@ let rec arity_sort = function let stre_of_cl = function | CL_SP sp -> - if is_constant sp then constant_strength sp else NeverDischarge + if is_constant sp then constant_or_parameter_strength sp + else NeverDischarge | CL_Var id -> variable_strength id | _ -> NeverDischarge @@ -323,7 +324,8 @@ let add_new_coercion_in_graph ((coef,xf),cls,clt) = let (inCoercion,outCoercion) = declare_object ("COERCION", { load_function = (fun _ -> ()); - open_function = (fun _ -> ()); + open_function = + (function (_,x) -> add_new_coercion_in_graph x); cache_function = (function (_,x) -> add_new_coercion_in_graph x); specification_function = (function x -> x) }) |