diff options
| author | herbelin | 2000-05-22 17:21:17 +0000 |
|---|---|---|
| committer | herbelin | 2000-05-22 17:21:17 +0000 |
| commit | 08f5f4b1268624de1f8733ce30b51a62080f6ba6 (patch) | |
| tree | a9cebdf444e0b1fdcd77e00d725a7905cafe6ff0 /tactics | |
| parent | abcf77362c7744ade443307d62dcb30e9025541a (diff) | |
suppression de l'env/sigma dans les fonctions de reduction beta et iota seuls
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@464 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 5 | ||||
| -rw-r--r-- | tactics/inv.ml | 4 | ||||
| -rw-r--r-- | tactics/tauto.ml | 2 |
3 files changed, 5 insertions, 6 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 86eb8113ec..955767cefb 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -791,7 +791,7 @@ let sig_clausale_forme env sigma sort_of_ty siglen ty (dFLT,dFLTty) = in (bindings,dFLT) else - let (a,p) = match whd_stack env sigma (whd_beta env sigma ty) [] with + let (a,p) = match whd_beta_stack ty [] with | (_,[a;p]) -> (a,p) | _ -> anomaly "sig_clausale_forme: should be a sigma type" in let mv = new_meta() in @@ -1200,7 +1200,8 @@ 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*) whd_betaiota env sigma app_B + env sigma *) + (* whd_betaiota *) app_B (* |- (P e2) BY RevSubstInConcl (eq T e1 e2) diff --git a/tactics/inv.ml b/tactics/inv.ml index 587890ca5f..e5a657e697 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -132,9 +132,7 @@ let make_inv_predicate env sigma ind id status concl = abstract_list_all env sigma p concl (realargs@[VAR id]) in let hyps,_ = decompose_lam pred in - let c3 = - whd_beta env sigma - (applist (pred,rel_list nrealargs (nrealargs +1))) + let c3 = whd_beta (applist (pred,rel_list nrealargs (nrealargs +1))) in (hyps,c3) in diff --git a/tactics/tauto.ml b/tactics/tauto.ml index 52b4e288c0..23b939b3cd 100644 --- a/tactics/tauto.ml +++ b/tactics/tauto.ml @@ -1703,7 +1703,7 @@ let tauto_of_cci_fmla gls cciterm = | _ -> assert false else FPred cciterm in - tradrec (whd_betaiota (pf_env gls) (project gls) cciterm) + tradrec (whd_betaiota cciterm) (*-- Retorna una lista de todas las variables proposicionales que aparescan en una lista de formulasS --*) |