diff options
| author | msozeau | 2006-05-29 19:59:11 +0000 |
|---|---|---|
| committer | msozeau | 2006-05-29 19:59:11 +0000 |
| commit | af354d63a814b0855eefda81852029d72b3544db (patch) | |
| tree | ef2fdf48eaea7e0690ac69cf9bc9b988c30bf11d /parsing | |
| parent | ba0bfcafe850586d72ad0b06db19d8de429d1caf (diff) | |
The "clean integration of subtac" patch.
Adds a new kind of casts (CastCoerce) for coercing an object to its base type (e.g. inductive).
The new cast_type type subsumes usual casts ConvCasts. Much of the patch is just adding ConvCasts where needed.
The Pretyping module has been adapted to this change, although it doesn't change anything yet, but this construct could have
a use with current coercions also. Pretyping is also cleaned from the "Use type constraints under lambdas" patch which is not yet ready
for wide use. It has been transferred to a copy of the Pretyping Functor in subtac_pretyping_F.ml.
Subtac is now working as well as I demonstrated at TYPES.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8875 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.ml4 | 8 | ||||
| -rw-r--r-- | parsing/g_proofs.ml4 | 2 | ||||
| -rw-r--r-- | parsing/g_xml.ml4 | 2 |
3 files changed, 6 insertions, 6 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 64d96ae4b6..82e1114256 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -28,7 +28,7 @@ let _ = List.iter (fun s -> Lexer.add_token("",s)) constr_kw let mk_cast = function (c,(_,None)) -> c - | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, DEFAULTcast,ty) + | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv DEFAULTcast, ty) let mk_lam = function ([],c) -> c @@ -155,8 +155,8 @@ GEXTEND Gram [ "200" RIGHTA [ c = binder_constr -> c ] | "100" RIGHTA - [ c1 = operconstr; ":"; c2 = binder_constr -> CCast(loc,c1,DEFAULTcast,c2) - | c1 = operconstr; ":"; c2 = SELF -> CCast(loc,c1,DEFAULTcast,c2) ] + [ c1 = operconstr; ":"; c2 = binder_constr -> CCast(loc,c1, CastConv DEFAULTcast,c2) + | c1 = operconstr; ":"; c2 = SELF -> CCast(loc,c1,CastConv DEFAULTcast,c2) ] | "99" RIGHTA [ ] | "90" RIGHTA [ c1 = operconstr; "->"; c2 = binder_constr -> CArrow(loc,c1,c2) @@ -320,7 +320,7 @@ GEXTEND Gram | "("; id=name; ":="; c=lconstr; ")" -> LocalRawDef (id,c) | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> - LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c,DEFAULTcast,t)) + LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv DEFAULTcast,t)) ] ] ; binder: diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 5d392846de..a1a7030990 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -117,6 +117,6 @@ GEXTEND Gram ; constr_body: [ [ ":="; c = lconstr -> c - | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c,Term.DEFAULTcast,t) ] ] + | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c, Rawterm.CastConv Term.DEFAULTcast,t) ] ] ; END diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 56be1ff5a8..bdedaf1764 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -181,7 +181,7 @@ let rec interp_xml_constr = function let ln,lc,lt = list_split3 (List.map interp_xml_CoFixFunction xl) in RRec (loc, RCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt) | XmlTag (loc,"CAST",al,[x1;x2]) -> - RCast (loc, interp_xml_term x1, DEFAULTcast, interp_xml_type x2) + RCast (loc, interp_xml_term x1, CastConv DEFAULTcast, interp_xml_type x2) | XmlTag (loc,"SORT",al,[]) -> RSort (loc, get_xml_sort al) | XmlTag (loc,s,_,_) -> user_err_loc (loc,"", str "Unexpected tag " ++ str s) |