diff options
| author | herbelin | 2002-01-18 15:27:45 +0000 |
|---|---|---|
| committer | herbelin | 2002-01-18 15:27:45 +0000 |
| commit | 96a51c9f3c1721b545c91b18e4d5af2b0864f165 (patch) | |
| tree | a70646953ea0b0a4cb27726832f37fc3bf6e183e | |
| parent | f84cc22a42f3563754dbeaa44fae88ab5fa6b198 (diff) | |
Le chargement des coercions est nécessaire même si le module n'est pas ouvert
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2409 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | lib/options.ml | 10 | ||||
| -rwxr-xr-x | pretyping/classops.ml | 10 |
2 files changed, 5 insertions, 15 deletions
diff --git a/lib/options.ml b/lib/options.ml index a8adcdb74e..8d49d6b759 100644 --- a/lib/options.ml +++ b/lib/options.ml @@ -49,16 +49,6 @@ let set_print_hyps_limit n = print_hyps_limit := Some n let unset_print_hyps_limit () = print_hyps_limit := None let print_hyps_limit () = !print_hyps_limit -let mes_ambig = ref true -let make_mes_ambig flag = mes_ambig:=flag -let is_mes_ambig() = !mes_ambig - -let without_mes_ambig f x = - let old = is_mes_ambig() in - try make_mes_ambig false; - let rslt = f x in (make_mes_ambig old; rslt) - with e -> (make_mes_ambig old; raise e) - (* A list of the areas of the system where "unsafe" operation * has been requested *) let unsafe_set = ref Stringset.empty diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 952bb98220..9590c3b765 100755 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -187,8 +187,8 @@ let cache_class (_,x) = add_new_class x let (inClass,outClass) = declare_object ("CLASS", - { load_function = (fun _ -> ()); - open_function = cache_class; + { load_function = cache_class; + open_function = (fun _ -> ()); cache_function = cache_class; export_function = (function x -> Some x) }) @@ -314,7 +314,7 @@ let add_coercion_in_graph (ic,source,target) = end) old_inheritance_graph end; - if (!ambig_paths <> []) && is_verbose () && is_mes_ambig() then + if (!ambig_paths <> []) && is_verbose () then ppnl (message_ambig !ambig_paths) type coercion = (coe_typ * coe_info_typ) * cl_typ * cl_typ @@ -332,8 +332,8 @@ let cache_coercion (_,((coe,xf),cls,clt)) = let (inCoercion,outCoercion) = declare_object ("COERCION", - { load_function = (fun _ -> ()); - open_function = cache_coercion; + { load_function = cache_coercion; + open_function = (fun _ -> ()); cache_function = cache_coercion; export_function = (function x -> Some x) }) |