diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/romega/refl_omega.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 570bb1877..d27b52259 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -219,7 +219,7 @@ let unintern_omega env id = calcul des variables utiles. *) let add_reified_atom t env = - try list_index0 t env.terms + try list_index0_f Term.eq_constr t env.terms with Not_found -> let i = List.length env.terms in env.terms <- env.terms @ [t]; i |