diff options
Diffstat (limited to 'plugins/nsatz')
| -rw-r--r-- | plugins/nsatz/nsatz.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index 8c3471a98..3a0d1dcbc 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -543,7 +543,7 @@ let nsatz lpol = let return_term t = let a = - mkApp(gen_constant "CC" ["Init";"Logic"] "refl_equal",[|tllp ();t|]) in + mkApp(gen_constant "CC" ["Init";"Logic"] "eq_refl",[|tllp ();t|]) in let a = EConstr.of_constr a in generalize [a] |