diff options
| author | barras | 2002-02-07 16:07:34 +0000 |
|---|---|---|
| committer | barras | 2002-02-07 16:07:34 +0000 |
| commit | 296faec482d17f9bfdc419f79ed565ecd8035e60 (patch) | |
| tree | 410123e747a8b3f3ca44aacb86f241c10360257a /proofs/logic.ml | |
| parent | 85bdcf8b1ca9b515d848878537755069ed03fd27 (diff) | |
petit nettoyage de kernel/inductive
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2460 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/logic.ml')
| -rw-r--r-- | proofs/logic.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index c6057367e8..5e920ea5ac 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -172,7 +172,7 @@ and mk_casegoals sigma goal goalacc p c = let pj = {uj_val=p; uj_type=pt} in let indspec = try find_mrectype env sigma ct - with Induc -> anomaly "mk_casegoals" in + with Not_found -> anomaly "mk_casegoals" in let (lbrty,conclty) = type_case_branches_with_names env indspec pj c in (acc'',lbrty,conclty) @@ -463,7 +463,7 @@ let prim_refiner r sigma goal = if k = 1 then try let _ = find_inductive env sigma c1 in () - with Induc -> + with Not_found -> error "cannot do a fixpoint on a non inductive type" else check_ind (k-1) b @@ -482,7 +482,7 @@ let prim_refiner r sigma goal = if k = 1 then try fst (find_inductive env sigma c1) - with Induc -> + with Not_found -> error "cannot do a fixpoint on a non inductive type" else check_ind (k-1) b @@ -513,7 +513,7 @@ let prim_refiner r sigma goal = | _ -> try let _ = find_coinductive env sigma b in () - with Induc -> + with Not_found -> error ("All methods must construct elements " ^ "in coinductive types") in |