From f5b2b3ac11763616acc7c418fa566554f2556b4a Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Thu, 31 Jul 2014 10:57:14 +0200 Subject: Untyped terms in ltac: simplify [coerce_to_uconstr]. Following advice by Hugo Herbelin. --- tactics/taccoerce.ml | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) (limited to 'tactics') diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml index b115311d9..415221819 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 -- cgit v1.2.3