diff options
| author | Arnaud Spiwack | 2014-07-31 10:57:14 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-08-01 19:18:58 +0200 |
| commit | f5b2b3ac11763616acc7c418fa566554f2556b4a (patch) | |
| tree | 48a7dc43dda772d9f076615af28b0c5dae3862a5 | |
| parent | 09b89545a5d349a29929965334963890740c05b7 (diff) | |
Untyped terms in ltac: simplify [coerce_to_uconstr].
Following advice by Hugo Herbelin.
| -rw-r--r-- | tactics/taccoerce.ml | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml index b115311d99..4152218197 100644 --- a/tactics/taccoerce.ml +++ b/tactics/taccoerce.ml @@ -152,11 +152,8 @@ let coerce_to_uconstr env v = if has_type v (topwit wit_uconstr) then out_gen (topwit wit_uconstr) v else - 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 (_ctx,c) = coerce_to_constr env v in + Detyping.detype false [] [] c let coerce_to_closed_constr env v = let ids,c = coerce_to_constr env v in |