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 /toplevel | |
| 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 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 2 | ||||
| -rw-r--r-- | toplevel/record.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index bfead59aaf..0f7f449cee 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -112,7 +112,7 @@ let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) = | Some comtyp -> (* We use a cast to avoid troubles with evars in comtyp *) (* that can only be resolved knowing com *) - let b = abstract_constr_expr (mkCastC (com,DEFAULTcast,comtyp)) bl in + let b = abstract_constr_expr (mkCastC (com, Rawterm.CastConv DEFAULTcast,comtyp)) bl in let (body,typ) = destSubCast (interp_constr sigma env b) in { const_entry_body = body; const_entry_type = Some typ; diff --git a/toplevel/record.ml b/toplevel/record.ml index f4f0c9150c..9c2d9732a3 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -36,7 +36,7 @@ let interp_decl sigma env = function | Vernacexpr.DefExpr((_,id),c,t) -> let c = match t with | None -> c - | Some t -> mkCastC (c,DEFAULTcast,t) + | Some t -> mkCastC (c, Rawterm.CastConv DEFAULTcast,t) in let j = interp_constr_judgment Evd.empty env c in (id,Some j.uj_val, j.uj_type) |