diff options
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") |