diff options
| author | barras | 2000-08-08 13:13:04 +0000 |
|---|---|---|
| committer | barras | 2000-08-08 13:13:04 +0000 |
| commit | b7e660c7115c479de49d026edd3a7c7c068b1f13 (patch) | |
| tree | 2fc04abd53d9fe33b06e3e99de3e7cf4e6cbafbe | |
| parent | 89a3416f68bddad29e80ed7d4f93b4a5ef418bd7 (diff) | |
reparation bug des coercions (cas ou on importe une coercion faisant
reference a une classe non importee)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@577 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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) }) |