diff options
| -rw-r--r-- | tactics/taccoerce.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml index 2c36398ed8..b115311d99 100644 --- a/tactics/taccoerce.ml +++ b/tactics/taccoerce.ml @@ -149,11 +149,14 @@ let coerce_to_constr env v = let coerce_to_uconstr env v = let v = Value.normalize v in - let fail () = raise (CannotCoerceTo "an untyped term") in if has_type v (topwit wit_uconstr) then out_gen (topwit wit_uconstr) v else - fail () + let (ctx,c) = coerce_to_constr env v in + (* spiwack: I'm not sure what I'm doing with this context. + May be wrong. *) + let ctx = List.map (fun id -> Name id) ctx in + Detyping.detype false [] ctx c let coerce_to_closed_constr env v = let ids,c = coerce_to_constr env v in |