aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega/Psatz.v
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega/Psatz.v')
-rw-r--r--plugins/micromega/Psatz.v5
1 files changed, 5 insertions, 0 deletions
diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v
index a3be56207..9e675165f 100644
--- a/plugins/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.v
@@ -74,3 +74,8 @@ Ltac lia :=
intros __wit __varmap __ff ;
change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity.
+
+
+(* Local Variables: *)
+(* coding: utf-8 *)
+(* End: *)