diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-02 22:58:48 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-02 22:58:48 +0000 |
| commit | 4318eefacae280fed3a159acfede35c568b2942b (patch) | |
| tree | fcbec538a568a7cc75af45fec579e121f84e2c77 /toplevel | |
| parent | 8404c8cd83aa8c802b628afe0c222b87bc7956ef (diff) | |
Modifs suite à intégration de class.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@192 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 25e29d703..20d0a40c1 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -735,11 +735,11 @@ let _ = definition_body_red id stre c red_option; message ((string_of_id id) ^ " is defined"); if coe then begin - Class.try_add_new_coercion (Some id) stre None None false; + Class.try_add_new_coercion id stre; message ((string_of_id id) ^ " is now a coercion") end; if idcoe then - Class.try_add_new_coercion None stre (Some (Left id)) None true; + Class.try_add_new_coercion_subclass stre id; if objdef then Recordobj.objdef_declare id | _ -> bad_vernac_args "DEFINITION") @@ -767,8 +767,7 @@ let _ = hypothesis_def_var (refining()) (string_of_id s) stre c; if coe then - Class.try_add_new_coercion (Some s) - stre None None false; + Class.try_add_new_coercion s stre; message ((string_of_id s) ^ " is assumed")) sl) slcl @@ -1142,8 +1141,7 @@ let _ = in let isid = identity = "IDENTITY" in fun () -> - Class.try_add_new_coercion (Some id) stre (Some (Left ids)) - (Some idt) isid; + Class.try_add_new_coercion id stre ids idt isid; message ((string_of_id id) ^ " is now a coercion") | _ -> bad_vernac_args "COERCION") ***) |