diff options
| author | herbelin | 2003-06-08 11:35:36 +0000 |
|---|---|---|
| committer | herbelin | 2003-06-08 11:35:36 +0000 |
| commit | 109b59d56b2c3b6d408075712375c9111feb2f20 (patch) | |
| tree | fdc9a07ff1113fb90ea5388e47fd678abf796388 /toplevel | |
| parent | 9955d65b30b4285d217feb4ae6ea5076e7579bf8 (diff) | |
Tables logarithmiques pour les coercions + nettoyage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4103 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/class.ml | 12 | ||||
| -rw-r--r-- | toplevel/discharge.ml | 2 |
2 files changed, 7 insertions, 7 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml index e1ba8e7368..75ab77bf08 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -82,14 +82,14 @@ let explain_coercion_error g = function | NoTarget -> (str"Cannot find the target class") | WrongTarget (clt,cl) -> - (str"Found target class " ++ str(string_of_class cl) ++ - str " while " ++ str(string_of_class clt) ++ + (str"Found target class " ++ pr_class cl ++ + str " while " ++ pr_class clt ++ str " is expected") | NotAClass ref -> (str "Type of " ++ Printer.pr_global ref ++ str " does not end with a sort") | NotEnoughClassArgs cl -> - (str"Wrong number of parameters for " ++str(string_of_class cl)) + (str"Wrong number of parameters for " ++ pr_class cl) (* Verifications pour l'ajout d'une classe *) @@ -123,7 +123,7 @@ let try_add_class cl streopt fail_if_exists = declare_class (cl,stre,p) else if fail_if_exists then errorlabstrm "try_add_new_class" - (str (string_of_class cl) ++ str " is already a class") + (pr_class cl ++ str " is already a class") (* Coercions *) @@ -222,7 +222,7 @@ let get_strength stre ref cls clt = let error_not_transparent source = errorlabstrm "build_id_coercion" - (str ((string_of_class source)^" must be a transparent constant")) + (pr_class source ++ str " must be a transparent constant") let build_id_coercion idf_opt source = let env = Global.env () in @@ -441,7 +441,7 @@ let process_cl sec_sp cl = cl | _ -> cl -let process_coercion olddir ids_to_discard ((coe,coeinfo),cls,clt) = +let process_coercion olddir ids_to_discard (coe,coeinfo,cls,clt) = let hyps = context_of_global_reference coe in let nargs = count_extra_abstractions hyps ids_to_discard in (process_global olddir coe, diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 1eb74c7e7f..d148a53435 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -253,7 +253,7 @@ let process_object oldenv olddir full_olddir newdir ((Class (y1,y2))::ops, ids_to_discard, work_alist) | "COERCION" -> - let (((_,coeinfo),_,_)as x) = outCoercion lobj in + let (_,coeinfo,_,_ as x) = outCoercion lobj in if coercion_strength coeinfo = Local then (ops,ids_to_discard,work_alist) else |