Untyped terms in tactic: add the possibility to use a typed term inside an untyped term.

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