diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-04 15:55:35 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-04 15:55:35 +0000 |
| commit | e9892fadb99ae56bf759c6013c7cccc07b31adab (patch) | |
| tree | a54568022a348f500daa3882146f93948fca1a91 /tactics | |
| parent | 65577c9f0c8a53f93b035063727d48af858bdab1 (diff) | |
Code mort
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@651 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 11 |
1 files changed, 1 insertions, 10 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index dcf09b5f1..e0a8c8541 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1175,16 +1175,7 @@ let subst_tuple_term env sigma dep_pair b = let abst_B = List.fold_right (fun (e,t) body -> lambda_create env (t,subst_term e body)) e_list b in - let app_B = applist(abst_B,proj_list) in - (* inutile ?? les projs sont appliquées à (mkRel 1) ?? *) -(* - let { proj1 = proj1_sp; proj2 = proj2_sp; elim = sig_elim_sp } = - find_sigma_data (get_sort_of env sigma typ) in - strong (fun _ _ -> - compose (whd_betaiota env sigma) - (whd_const [proj1_sp;proj2_sp;sig_elim_sp] env sigma)) - env sigma *) - (* whd_betaiota *) app_B + let app_B = applist(abst_B,proj_list) in app_B (* |- (P e2) BY RevSubstInConcl (eq T e1 e2) |