diff options
| author | herbelin | 2000-10-11 20:03:05 +0000 |
|---|---|---|
| committer | herbelin | 2000-10-11 20:03:05 +0000 |
| commit | 7f7fa0184ea32c81e77d34683bca8e456b80a19a (patch) | |
| tree | 6480027178a4e50c5ecc1980f93d52b1d69612b9 /proofs | |
| parent | 9386577e2f67c49c2c7b6bab00cd6dc4a5b3b513 (diff) | |
Renommage des find_m*type
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@693 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -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 9aeff1f28a..0e5b970c90 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -355,7 +355,7 @@ let prim_refiner r sigma goal = | IsProd (_,c1,b) -> if k = 1 then try - let _ = find_minductype env sigma c1 in () + let _ = find_inductive env sigma c1 in () with Induc -> error "cannot do a fixpoint on a non inductive type" else @@ -375,7 +375,7 @@ let prim_refiner r sigma goal = | IsProd (_,c1,b) -> if k = 1 then try - fst (find_minductype env sigma c1) + fst (find_inductive env sigma c1) with Induc -> error "cannot do a fixpoint on a non inductive type" else @@ -407,7 +407,7 @@ let prim_refiner r sigma goal = | IsProd (_,c1,b) -> check_is_coind b | _ -> try - let _ = find_mcoinductype env sigma b in () + let _ = find_coinductive env sigma b in () with Induc -> error ("All methods must construct elements " ^ "in coinductive types") |