diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-01 14:54:09 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-01 14:54:09 +0000 |
| commit | 9bfe45ef4974157c18ef18876b7df8adfb286414 (patch) | |
| tree | e4d6620376a697196908a6f153c3e4df7f18c72e /tactics/elim.mli | |
| parent | ece6204d9ccb8e37f5050ba4ee5c3d43669bf6ef (diff) | |
Déplacement définition intro_pattern_expr dans Genarg
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5406 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/elim.mli')
| -rw-r--r-- | tactics/elim.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/elim.mli b/tactics/elim.mli index 0fb104310..4aeea9981 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -13,6 +13,7 @@ open Names open Term open Proof_type open Tacmach +open Genarg open Tacticals (*i*) @@ -22,7 +23,7 @@ val introElimAssumsThen : (branch_assumptions -> tactic) -> branch_args -> tactic val introCaseAssumsThen : - (Tacexpr.intro_pattern_expr list -> branch_assumptions -> tactic) -> + (intro_pattern_expr list -> branch_assumptions -> tactic) -> branch_args -> tactic val general_decompose : (identifier * constr -> bool) -> constr -> tactic |