From beed52ca495d7cceac9abba5722576a6d9f15ed2 Mon Sep 17 00:00:00 2001 From: delahaye Date: Fri, 5 Jan 2001 19:45:07 +0000 Subject: Arite cachee de Match Context + Meta Definition git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1236 85f007b7-540e-0410-9357-904b9bb8a0f7 --- proofs/tacinterp.mli | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) (limited to 'proofs/tacinterp.mli') diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli index a23f953e6..67bd209e3 100644 --- a/proofs/tacinterp.mli +++ b/proofs/tacinterp.mli @@ -16,19 +16,20 @@ type value = | VTactic of tactic | VFTactic of tactic_arg list * (tactic_arg list -> tactic) | VRTactic of (goal list sigma * validation) + | VContext of (interp_sign -> goal sigma -> value) | VArg of tactic_arg | VFun of (string * value) list * string option list * Coqast.t | VVoid | VRec of value ref +(* Signature for interpretation: val_interp and interpretation functions *) +and interp_sign = + enamed_declarations * Environ.env * (string * value) list * + (int * constr) list * goal sigma option * debug_info + (* Gives the constr corresponding to a CONSTR [tactic_arg] *) val constr_of_Constr : tactic_arg -> constr -(* Signature for interpretation: [val_interp] and interpretation functions *) -type interp_sign = - enamed_declarations * Environ.env * (string * value) list * - (int * constr) list * goal sigma option * debug_info - (* To provide the tactic expressions *) val loc : Coqast.loc val tacticIn : (unit -> Coqast.t) -> Coqast.t @@ -48,8 +49,8 @@ val set_debug : debug_info -> unit (* Gives the state of debug *) val get_debug : unit -> debug_info -(* Adds a Tactic Definition in the table *) -val add_tacdef : string -> Coqast.t -> unit +(* Adds a Meta Definition in the table *) +val add_metadef : string -> Coqast.t -> unit (* Interprets any expression *) val val_interp : interp_sign -> Coqast.t -> value -- cgit v1.2.3