diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_type.mli | 7 | ||||
| -rw-r--r-- | proofs/tacinterp.mli | 45 |
2 files changed, 28 insertions, 24 deletions
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index eaebd6b992..9c2ac00ae4 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -1,3 +1,6 @@ + +(* $Id$ *) + (*i*) open Environ open Evd @@ -7,8 +10,8 @@ open Term open Util (*i*) -(*This module defines the structure of proof tree and the tactic type. So, it - is used by Proof_tree and Refiner*) +(* This module defines the structure of proof tree and the tactic type. So, it + is used by [Proof_tree] and [Refiner] *) type bindOcc = | Dep of identifier diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli index 87d5e2a1ff..9f82d30e7b 100644 --- a/proofs/tacinterp.mli +++ b/proofs/tacinterp.mli @@ -9,37 +9,38 @@ open Tacmach open Term (*i*) -(*Values for interpretation*) -type value= - VTactic of tactic - |VFTactic of tactic_arg list*(tactic_arg list->tactic) - |VRTactic of (goal list sigma * validation) - |VArg of tactic_arg - |VFun of (string*value) list*string option list*Coqast.t - |VVoid - |VRec of value ref;; +(* Values for interpretation *) +type value = + | VTactic of tactic + | VFTactic of tactic_arg list * (tactic_arg list -> tactic) + | VRTactic of (goal list sigma * validation) + | VArg of tactic_arg + | VFun of (string * value) list * string option list * Coqast.t + | VVoid + | VRec of value ref -(*Gives the constr corresponding to a CONSTR tactic_arg*) -val constr_of_Constr:tactic_arg-> constr;; +(* 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= - evar_declarations*Environ.env*(string*value) list*(int*constr) list* - goal sigma option;; +(* Signature for interpretation: [val_interp] and interpretation functions *) +type interp_sign = + evar_declarations * Environ.env * (string * value) list * + (int * constr) list * goal sigma option -(*Adds a Tactic Definition in the table*) -val add_tacdef : string -> value -> unit;; +(* Adds a Tactic Definition in the table *) +val add_tacdef : string -> value -> unit -(*Interprets any expression*) -val val_interp:interp_sign->Coqast.t->value;; +(*Interprets any expression *) +val val_interp : interp_sign -> Coqast.t -> value + +(* Interprets tactic arguments *) +val interp_tacarg : interp_sign -> Coqast.t -> tactic_arg -(*Interprets tactic arguments*) -val interp_tacarg:interp_sign->Coqast.t->tactic_arg;; val interp : Coqast.t -> tactic val vernac_interp : Coqast.t -> tactic val vernac_interp_atomic : identifier -> tactic_arg list -> tactic -val is_just_undef_macro : Coqast.t -> string option +val is_just_undef_macro : Coqast.t -> string option val bad_tactic_args : string -> 'a |