diff options
| author | herbelin | 2000-05-31 11:46:29 +0000 |
|---|---|---|
| committer | herbelin | 2000-05-31 11:46:29 +0000 |
| commit | 301d5af223390fa5c82da9ae9958f610493ba814 (patch) | |
| tree | 304f4b7b194ace4c6fac67af90a0bcdf3ff3537f /tactics | |
| parent | aca8a6bbb4fa372cd3b27680eee642082d1c2ad5 (diff) | |
Nettoyage de Generic
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@482 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 5 | ||||
| -rw-r--r-- | tactics/wcclausenv.ml | 4 |
2 files changed, 4 insertions, 5 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 955767cefb..c923cfe171 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -726,7 +726,7 @@ let make_tuple env sigma (rterm,rty) lind = find_sigma_data (get_sort_of env sigma rty) in let a = type_of env sigma (Rel lind) in (* We replace (Rel lind) by (Rel 1) in rty then abstract on (na:a) *) - let rty' = substn_many [|make_substituend (Rel 1)|] lind rty in + let rty' = substnl [Rel 1] lind rty in let na = fst (lookup_rel lind env) in let p = mkLambda na a rty' in (applist(exist_term,[a;p;(Rel lind);rterm]), @@ -1228,8 +1228,7 @@ let substInHyp eqn id gls = let (lbeq,(t,e1,e2)) = (find_eq_data_decompose eqn) in let body = subst_term e1 (clause_type (Some id) gls) in if not (dependent (Rel 1) body) then errorlabstrm "SubstInHyp" [<>]; - let pB = DLAM(Environ.named_hd (pf_env gls) t Anonymous,body) in - (tclTHENS (cut_replacing id (sAPP pB e2)) + (tclTHENS (cut_replacing id (subst1 e2 body)) ([tclIDTAC; (tclTHENS (bareRevSubstInConcl lbeq body (t,e1,e2)) ([exact (VAR id);tclIDTAC]))])) gls diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml index 8a76a0e6fa..48ae03cc92 100644 --- a/tactics/wcclausenv.ml +++ b/tactics/wcclausenv.ml @@ -134,9 +134,9 @@ let elim_res_pf_THEN_i kONT clenv tac gls = let rec build_args acc ce p_0 p_1 = match p_0,p_1 with - | ((DOP2(Prod,a,(DLAM(na,_) as b))), (a_0::bargs)) -> + | ((DOP2(Prod,a,DLAM(na,b))), (a_0::bargs)) -> let (newa,ce') = (build_term ce (na,Some a) a_0) in - build_args (newa::acc) ce' (sAPP b a_0) bargs + build_args (newa::acc) ce' (subst1 a_0 b) bargs | (_, []) -> (List.rev acc,ce) | (_, (_::_)) -> failwith "mk_clenv_using" |