diff options
author | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
commit | 870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch) | |
tree | 0c647056de1832cf1dba5ba58758b9121418e4be /tactics/equality.mli | |
parent | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff) |
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'tactics/equality.mli')
-rw-r--r-- | tactics/equality.mli | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/tactics/equality.mli b/tactics/equality.mli index 42c502be..f05ebc6c 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -6,9 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: equality.mli 11166 2008-06-22 13:23:35Z herbelin $ i*) +(*i $Id: equality.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) (*i*) +open Util open Names open Term open Sign @@ -45,6 +46,7 @@ val rewriteRL : constr -> tactic val register_general_setoid_rewrite_clause : (identifier option -> bool -> occurrences -> constr -> new_goals:constr list -> tactic) -> unit +val register_is_applied_setoid_relation : (constr -> bool) -> unit val general_rewrite_bindings_in : bool -> occurrences -> identifier -> constr with_bindings -> evars_flag -> tactic @@ -74,9 +76,9 @@ val discrHyp : identifier -> tactic val discrEverywhere : evars_flag -> tactic val discr_tac : evars_flag -> constr with_ebindings induction_arg option -> tactic -val inj : intro_pattern_expr list -> evars_flag -> +val inj : intro_pattern_expr located list -> evars_flag -> constr with_ebindings -> tactic -val injClause : intro_pattern_expr list -> evars_flag -> +val injClause : intro_pattern_expr located list -> evars_flag -> constr with_ebindings induction_arg option -> tactic val injHyp : identifier -> tactic val injConcl : tactic |