diff options
| author | Pierre-Marie Pédrot | 2017-07-28 17:53:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-07-30 00:20:30 +0200 |
| commit | 0f72b089de52ad7d26d71e56003b140fa5012635 (patch) | |
| tree | 9fe0d82fc1c30e0a4740dfc23a876e0a8aa817a9 /src/tac2core.ml | |
| parent | 23f10f3a1a0fd6498cad975b39af5dd3a8559f06 (diff) | |
Exporting more internals from Coq implementation.
Diffstat (limited to 'src/tac2core.ml')
| -rw-r--r-- | src/tac2core.ml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml index f28c5c5dcf..515cadc525 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -557,6 +557,14 @@ let prm_refine : ml_tactic = function end >>= fun () -> return v_unit | _ -> assert false +let prm_with_holes : ml_tactic = function +| [x; f] -> + Proofview.tclEVARMAP >>= fun sigma0 -> + thaw x >>= fun ans -> + Proofview.tclEVARMAP >>= fun sigma -> + Proofview.Unsafe.tclEVARS sigma0 >>= fun () -> + Tacticals.New.tclWITHHOLES false (interp_app f [ans]) sigma +| _ -> assert false (** Registering *) @@ -615,6 +623,7 @@ let () = Tac2env.define_primitive (pname "goal") prm_goal let () = Tac2env.define_primitive (pname "hyp") prm_hyp let () = Tac2env.define_primitive (pname "hyps") prm_hyps let () = Tac2env.define_primitive (pname "refine") prm_refine +let () = Tac2env.define_primitive (pname "with_holes") prm_with_holes (** ML types *) |