Rolling up our own representation of clauses.

1 files changed, 16 insertions, 11 deletions

diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli
index 842b09c22f..3d64e7ec8c 100644
--- a/src/tac2tactics.mli
+++ b/src/tac2tactics.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Locus
 open Globnames
 open Tac2expr
 open EConstr
@@ -31,6 +30,8 @@ val elim : evars_flag -> constr_with_bindings -> constr_with_bindings option ->
 
 val general_case_analysis : evars_flag -> constr_with_bindings ->  unit tactic
 
+val generalize : (constr * occurrences * Name.t) list -> unit tactic
+
 val constructor_tac : evars_flag -> int option -> int -> bindings -> unit tactic
 
 val left_with_bindings  : evars_flag -> bindings -> unit tactic
@@ -40,6 +41,8 @@ val split_with_bindings : evars_flag -> bindings -> unit tactic
 val rewrite :
   evars_flag -> rewriting list -> clause -> unit tactic option -> unit tactic
 
+val symmetry : clause -> unit tactic
+
 val forward : bool -> unit tactic option option ->
   intro_pattern option -> constr -> unit tactic
 
@@ -48,8 +51,10 @@ val assert_ : assertion -> unit tactic
 val letin_pat_tac : evars_flag -> (bool * intro_pattern_naming) option ->
   Name.t -> (Evd.evar_map * constr) -> clause -> unit tactic
 
+val reduce : Redexpr.red_expr -> clause -> unit tactic
+
 val simpl : global_reference glob_red_flag ->
-  (Pattern.constr_pattern * occurrences_expr) option -> clause -> unit tactic
+  (Pattern.constr_pattern * occurrences) option -> clause -> unit tactic
 
 val cbv : global_reference glob_red_flag -> clause -> unit tactic
 
@@ -57,20 +62,20 @@ val cbn : global_reference glob_red_flag -> clause -> unit tactic
 
 val lazy_ : global_reference glob_red_flag -> clause -> unit tactic
 
-val unfold : (global_reference * occurrences_expr) list -> clause -> unit tactic
+val unfold : (global_reference * occurrences) list -> clause -> unit tactic
 
-val pattern : (constr * occurrences_expr) list -> clause -> unit tactic
+val pattern : (constr * occurrences) list -> clause -> unit tactic
 
-val vm : (Pattern.constr_pattern * occurrences_expr) option -> clause -> unit tactic
+val vm : (Pattern.constr_pattern * occurrences) option -> clause -> unit tactic
 
-val native : (Pattern.constr_pattern * occurrences_expr) option -> clause -> unit tactic
+val native : (Pattern.constr_pattern * occurrences) option -> clause -> unit tactic
 
 val eval_red : constr -> constr tactic
 
 val eval_hnf : constr -> constr tactic
 
 val eval_simpl : global_reference glob_red_flag ->
-  (Pattern.constr_pattern * occurrences_expr) option -> constr -> constr tactic
+  (Pattern.constr_pattern * occurrences) option -> constr -> constr tactic
 
 val eval_cbv : global_reference glob_red_flag -> constr -> constr tactic
 
@@ -78,15 +83,15 @@ val eval_cbn : global_reference glob_red_flag -> constr -> constr tactic
 
 val eval_lazy : global_reference glob_red_flag -> constr -> constr tactic
 
-val eval_unfold : (global_reference * occurrences_expr) list -> constr -> constr tactic
+val eval_unfold : (global_reference * occurrences) list -> constr -> constr tactic
 
 val eval_fold : constr list -> constr -> constr tactic
 
-val eval_pattern : (EConstr.t * occurrences_expr) list -> constr -> constr tactic
+val eval_pattern : (EConstr.t * occurrences) list -> constr -> constr tactic
 
-val eval_vm : (Pattern.constr_pattern * occurrences_expr) option -> constr -> constr tactic
+val eval_vm : (Pattern.constr_pattern * occurrences) option -> constr -> constr tactic
 
-val eval_native : (Pattern.constr_pattern * occurrences_expr) option -> constr -> constr tactic
+val eval_native : (Pattern.constr_pattern * occurrences) option -> constr -> constr tactic
 
 val discriminate : evars_flag -> destruction_arg option -> unit tactic