diff options
| author | herbelin | 2000-10-01 13:37:35 +0000 |
|---|---|---|
| committer | herbelin | 2000-10-01 13:37:35 +0000 |
| commit | 3dc7ac2dcfdf8e8255a23c868de29a03a11ceb2e (patch) | |
| tree | 566494b556261e2578614b0b2168837b3e3ec66a | |
| parent | a69a9d0c3792da57dfbc513d47c2a36dd3328ab3 (diff) | |
Plus de whd_castapp
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@624 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | proofs/logic.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 3b7c85b405..77c6a996ef 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -359,7 +359,7 @@ let prim_refiner r sigma goal = | { name = Fix; hypspecs = []; terms = []; newids = [f]; params = [Num(_,n)] } -> let rec check_ind k cl = - match kind_of_term (whd_castapp cl) with + match kind_of_term (strip_outer_cast cl) with | IsProd (_,c1,b) -> if k = 1 then try @@ -379,7 +379,7 @@ let prim_refiner r sigma goal = | { name = Fix; hypspecs = []; terms = lar; newids = lf; params = ln } -> let rec check_ind k cl = - match kind_of_term (whd_castapp cl) with + match kind_of_term (strip_outer_cast cl) with | IsProd (_,c1,b) -> if k = 1 then try @@ -410,7 +410,7 @@ let prim_refiner r sigma goal = | { name = Cofix; hypspecs = []; terms = lar; newids = lf; params = [] } -> let rec check_is_coind cl = - let b = whd_betadeltaiota env sigma (whd_castapp cl) in + let b = whd_betadeltaiota env sigma cl in match kind_of_term b with | IsProd (_,c1,b) -> check_is_coind b | _ -> |