diff options
Diffstat (limited to 'src/tac2stdlib.ml')
| -rw-r--r-- | src/tac2stdlib.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml index 28bcd6a1cf..0db71fb293 100644 --- a/src/tac2stdlib.ml +++ b/src/tac2stdlib.ml @@ -294,13 +294,12 @@ let () = define_prim2 "tac_pose" begin fun idopt c -> Tactics.letin_tac None na c None Locusops.nowhere end -let () = define_prim4 "tac_set" begin fun ev idopt c cl -> +let () = define_prim3 "tac_set" begin fun ev p cl -> let ev = Value.to_bool ev in - let na = to_name idopt in let cl = to_clause cl in Proofview.tclEVARMAP >>= fun sigma -> - thaw c >>= fun c -> - let c = Value.to_constr c in + thaw p >>= fun p -> + let (na, c) = to_pair to_name Value.to_constr p in Tactics.letin_pat_tac ev None na (sigma, c) cl end |