diff options
| author | herbelin | 2000-05-18 18:06:17 +0000 |
|---|---|---|
| committer | herbelin | 2000-05-18 18:06:17 +0000 |
| commit | 9bb76e1a6d31b98214a87af3bc69455ae90dcf38 (patch) | |
| tree | 6cd39ae794f9c8422a04681ee98997da6d0a01cf /tactics/equality.ml | |
| parent | 391e26950408b9a54fb09b55bbaed6dde4fc208e (diff) | |
bugs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@453 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 1e3770ad00..86eb8113ec 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1200,7 +1200,7 @@ let subst_tuple_term env sigma dep_pair b = strong (fun _ _ -> compose (whd_betaiota env sigma) (whd_const [proj1_sp;proj2_sp;sig_elim_sp] env sigma)) - env sigma*) app_B + env sigma*) whd_betaiota env sigma app_B (* |- (P e2) BY RevSubstInConcl (eq T e1 e2) @@ -1210,7 +1210,7 @@ let subst_tuple_term env sigma dep_pair b = let revSubstInConcl eqn gls = let (lbeq,(t,e1,e2)) = find_eq_data_decompose eqn in let body = subst_tuple_term (pf_env gls) (project gls) e2 (pf_concl gls) in - assert (not (dependent (Rel 1) body)); + assert (dependent (Rel 1) body); bareRevSubstInConcl lbeq body (t,e1,e2) gls (* |- (P e1) |