diff options
Diffstat (limited to 'proofs/proof_type.ml')
-rw-r--r-- | proofs/proof_type.ml | 24 |
1 files changed, 14 insertions, 10 deletions
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 6f4cf4640..b905c0a26 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -18,6 +18,8 @@ open Util open Tacexpr open Rawterm open Genarg +open Nametab +open Pattern (*i*) (* This module defines the structure of proof tree and the tactic type. So, it @@ -67,31 +69,33 @@ and validation = (proof_tree list -> proof_tree) and tactic_expr = (constr, + constr_pattern, evaluable_global_reference, inductive or_metanum, - identifier) + ltac_constant, + identifier, + glob_tactic_expr) Tacexpr.gen_tactic_expr and atomic_tactic_expr = (constr, + constr_pattern, evaluable_global_reference, inductive or_metanum, - identifier) + ltac_constant, + identifier, + glob_tactic_expr) Tacexpr.gen_atomic_tactic_expr and tactic_arg = (constr, + constr_pattern, evaluable_global_reference, inductive or_metanum, - identifier) + ltac_constant, + identifier, + glob_tactic_expr) Tacexpr.gen_tactic_arg type hyp_location = identifier Tacexpr.raw_hyp_location -type open_generic_argument = - (constr,raw_tactic_expr) generic_argument -type closed_generic_argument = - (constr,raw_tactic_expr) generic_argument - -type 'a closed_abstract_argument_type = - ('a,constr,raw_tactic_expr) abstract_argument_type |