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 /interp | |
| 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 'interp')
| -rw-r--r-- | interp/topconstr.ml | 6 | ||||
| -rw-r--r-- | interp/topconstr.mli | 6 |
2 files changed, 6 insertions, 6 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 7a634a71a4..5b9b404425 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -45,7 +45,7 @@ type aconstr = | ASort of rawsort | AHole of Evd.hole_kind | APatVar of patvar - | ACast of aconstr * cast_kind * aconstr + | ACast of aconstr * cast_type * aconstr let name_app f e = function | Name id -> let (id, e) = f id e in (e, Name id) @@ -94,7 +94,7 @@ let rawconstr_of_aconstr_with_binders loc g f e = function | AIf (c,(na,po),b1,b2) -> let e,na = name_app g e na in RIf (loc,f e c,(na,option_map (f e) po),f e b1,f e b2) - | ACast (c,k,t) -> RCast (loc,f e c,k,f e t) + | ACast (c,k,t) -> RCast (loc,f e c, k,f e t) | ASort x -> RSort (loc,x) | AHole x -> RHole (loc,x) | APatVar n -> RPatVar (loc,(false,n)) @@ -524,7 +524,7 @@ type constr_expr = | CPatVar of loc * (bool * patvar) | CEvar of loc * existential_key | CSort of loc * rawsort - | CCast of loc * constr_expr * cast_kind * constr_expr + | CCast of loc * constr_expr * cast_type * constr_expr | CNotation of loc * notation * constr_expr list | CPrim of loc * prim_token | CDelimiters of loc * string * constr_expr diff --git a/interp/topconstr.mli b/interp/topconstr.mli index d5b718d343..9173d3116e 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -41,7 +41,7 @@ type aconstr = | ASort of rawsort | AHole of Evd.hole_kind | APatVar of patvar - | ACast of aconstr * cast_kind * aconstr + | ACast of aconstr * cast_type * aconstr val rawconstr_of_aconstr_with_binders : loc -> (identifier -> 'a -> identifier * 'a) -> @@ -107,7 +107,7 @@ type constr_expr = | CPatVar of loc * (bool * patvar) | CEvar of loc * existential_key | CSort of loc * rawsort - | CCast of loc * constr_expr * cast_kind * constr_expr + | CCast of loc * constr_expr * cast_type * constr_expr | CNotation of loc * notation * constr_expr list | CPrim of loc * prim_token | CDelimiters of loc * string * constr_expr @@ -143,7 +143,7 @@ val names_of_cases_indtype : constr_expr -> identifier list val mkIdentC : identifier -> constr_expr val mkRefC : reference -> constr_expr val mkAppC : constr_expr * constr_expr list -> constr_expr -val mkCastC : constr_expr * cast_kind * constr_expr -> constr_expr +val mkCastC : constr_expr * cast_type * constr_expr -> constr_expr val mkLambdaC : name located list * constr_expr * constr_expr -> constr_expr val mkLetInC : name located * constr_expr * constr_expr -> constr_expr val mkProdC : name located list * constr_expr * constr_expr -> constr_expr |