diff options
| -rw-r--r-- | src/tac2core.ml | 32 | ||||
| -rw-r--r-- | theories/Constr.v | 5 |
2 files changed, 37 insertions, 0 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml index 0304286639..468fddaddf 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -494,6 +494,38 @@ let () = define3 "constr_closenl" (list ident) int constr begin fun ids k c -> return (Value.of_constr ans) end +let () = define3 "constr_in_context" ident constr closure begin fun id t c -> + Proofview.Goal.goals >>= function + | [gl] -> + gl >>= fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let has_var = + try + let _ = Environ.lookup_named_val id (Environ.named_context_val env) in + true + with Not_found -> false + in + if has_var then + Tacticals.New.tclZEROMSG (str "Variable already exists") + else + let open Context.Named.Declaration in + let nenv = EConstr.push_named (LocalAssum (id, t)) env in + let (sigma, (evt, _)) = Evarutil.new_type_evar nenv sigma Evd.univ_flexible in + let (sigma, evk) = Evarutil.new_pure_evar (Environ.named_context_val nenv) sigma evt in + Proofview.Unsafe.tclEVARS sigma >>= fun () -> + Proofview.Unsafe.tclSETGOALS [evk] >>= fun () -> + thaw c >>= fun _ -> + Proofview.Unsafe.tclSETGOALS [Proofview.Goal.goal (Proofview.Goal.assume gl)] >>= fun () -> + let args = List.map (fun d -> EConstr.mkVar (get_id d)) (EConstr.named_context env) in + let args = Array.of_list (EConstr.mkRel 1 :: args) in + let ans = EConstr.mkEvar (evk, args) in + let ans = EConstr.mkLambda (Name id, t, ans) in + return (Value.of_constr ans) + | _ -> + throw err_notfocussed +end + (** Patterns *) let () = define2 "pattern_matches" pattern constr begin fun pat c -> diff --git a/theories/Constr.v b/theories/Constr.v index 3e67a486cf..072c613920 100644 --- a/theories/Constr.v +++ b/theories/Constr.v @@ -58,3 +58,8 @@ Ltac2 @ external closenl : ident list -> int -> constr -> constr := "ltac2" "con [Rel(k); ...; Rel(k+n-1)] in [c]. If two names are identical, the one of least index is kept. *) End Unsafe. + +Ltac2 @ external in_context : ident -> constr -> (unit -> unit) -> constr := "ltac2" "constr_in_context". +(** On a focussed goal [Γ ⊢ A], [in_context id c tac] evaluates [tac] in a + focussed goal [Γ, id : c ⊢ ?X] and returns [fun (id : c) => t] where [t] is + the proof built by the tactic. *) |