diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-24 17:56:05 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-24 17:56:05 +0000 |
| commit | 33c03c270a2380c8462914b02c3355d4a5cea273 (patch) | |
| tree | ba4523cbe3a09608a623b71ef63183aacdec8aaa /tactics/equality.mli | |
| parent | 5a09134ebee8d92d9ed05d04d2808a30a2d83900 (diff) | |
Simplifications concommitantes à la correction du bug #855
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6126 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/equality.mli')
| -rw-r--r-- | tactics/equality.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tactics/equality.mli b/tactics/equality.mli index 6b405b247..672c4014a 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -55,8 +55,7 @@ val dEq : quantified_hypothesis option -> tactic val dEqThen : (int -> tactic) -> quantified_hypothesis option -> tactic val make_iterated_tuple : - env -> evar_map -> (constr * constr) -> (constr * constr) - -> constr * constr * constr + env -> evar_map -> constr -> (constr * types) -> constr * constr * constr val substHypInConcl : bool -> identifier -> tactic val substConcl : bool -> constr -> tactic |