diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2013-09-06 22:01:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2013-11-27 18:43:35 +0100 |
| commit | 982c1ae49d200f782a5b82f53164d68418a77387 (patch) | |
| tree | c0cd589357a3152fade6e19de76764d6ab634023 | |
| parent | 144f2ac7c7394a701808daa503a0b6ded5663fcc (diff) | |
Adding the necessary hooks to handle tactics in terms.
| -rw-r--r-- | interp/genintern.ml | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 19 |
2 files changed, 21 insertions, 0 deletions
diff --git a/interp/genintern.ml b/interp/genintern.ml index 86a1ce1f5..d1bc28333 100644 --- a/interp/genintern.ml +++ b/interp/genintern.ml @@ -54,3 +54,5 @@ let register_subst0 = Subst.register0 let generic_substitute subs v = let unpack wit v = in_gen (glbwit wit) (substitute wit subs v) in glb_unpack { glb_unpack = unpack; } v + +let () = Hook.set Detyping.subst_genarg_hook generic_substitute diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 845b3ad9f..0821423b5 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2188,6 +2188,25 @@ let tacticIn t = (***************************************************************************) (* Backwarding recursive needs of tactic glob/interp/eval functions *) +let _ = + let eval ty env sigma lfun arg = + let ist = { lfun = lfun; extra = TacStore.empty; } in + if has_type arg (glbwit wit_tactic) then + let tac = out_gen (glbwit wit_tactic) arg in + let tac = interp_tactic ist tac in + let prf = Proof.start sigma [env, ty] in + let (prf, _) = Proof.run_tactic env tac prf in + let sigma = Proof.in_proof prf (fun sigma -> sigma) in + let ans = match Proof.initial_goals prf with + | [c, _] -> c + | _ -> assert false + in + ans, sigma + else + failwith "not a tactic" + in + Hook.set Pretyping.genarg_interp_hook eval + let _ = Hook.set Auto.extern_interp (fun l -> let lfun = Id.Map.map (fun c -> Value.of_constr c) l in |