diff options
| author | herbelin | 2000-10-01 13:36:51 +0000 |
|---|---|---|
| committer | herbelin | 2000-10-01 13:36:51 +0000 |
| commit | a69a9d0c3792da57dfbc513d47c2a36dd3328ab3 (patch) | |
| tree | 4c1fe0ec501fe9eea80c3a1d628714c44e22cc9a /tactics | |
| parent | 3608aa2e376bf7ed1ad7d04ffe99ffde06e9775b (diff) | |
Plus de whd_castapp_stack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@623 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 6c4665fd35..3f864682e4 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -814,7 +814,7 @@ let new_hyp mopt c blist g = let (wc,kONT) = startWalk g in let clause = mk_clenv_printable_type_of wc c in let clause' = clenv_match_args blist clause in - let (thd,tstack) = whd_castapp_stack (clenv_instance_template clause')[] in + let (thd,tstack) = whd_stack (clenv_instance_template clause') in let nargs = List.length tstack in let cut_pf = applist(thd, @@ -1089,7 +1089,8 @@ let atomize_param_of_ind hyp0 gl = if i<>nparams then let tmptyp0 = pf_get_hyp_typ gl hyp0 in let (_,indtyp,_) = pf_reduce_to_mind gl tmptyp0 in - match kind_of_term (destAppL (whd_castapp indtyp)).(i) with + let argl = snd (decomp_app indtyp) in + match kind_of_term (List.index argl (i-1)) with | IsVar id when not (List.exists (occur_var id) avoid) -> atomize_one (i-1) ((mkVar id)::avoid) gl | IsVar id -> |