aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/romega/refl_omega.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/romega/refl_omega.ml')
-rw-r--r--plugins/romega/refl_omega.ml5
1 files changed, 3 insertions, 2 deletions
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 79db4a9c4..e8a72c055 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -225,7 +225,7 @@ let add_reified_atom t env =
env.terms <- env.terms @ [t]; i
let get_reified_atom env =
- try List.nth env.terms with _ -> failwith "get_reified_atom"
+ try List.nth env.terms with Invalid_argument _ -> failwith "get_reified_atom"
(* \subsection{Gestion de l'environnement de proposition pour Omega} *)
(* ajout d'une proposition *)
@@ -235,7 +235,8 @@ let add_prop env t =
let i = List.length env.props in env.props <- env.props @ [t]; i
(* accès a une proposition *)
-let get_prop v env = try List.nth v env with _ -> failwith "get_prop"
+let get_prop v env =
+ try List.nth v env with Invalid_argument _ -> failwith "get_prop"
(* \subsection{Gestion du nommage des équations} *)
(* Ajout d'une equation dans l'environnement de reification *)