aboutsummaryrefslogtreecommitdiff
path: root/coqprime/gencertif/factorize.h
diff options
context:
space:
mode:
Diffstat (limited to 'coqprime/gencertif/factorize.h')
-rw-r--r--coqprime/gencertif/factorize.h21
1 files changed, 21 insertions, 0 deletions
diff --git a/coqprime/gencertif/factorize.h b/coqprime/gencertif/factorize.h
new file mode 100644
index 000000000..d61e87b83
--- /dev/null
+++ b/coqprime/gencertif/factorize.h
@@ -0,0 +1,21 @@
+/*
+(*************************************************************)
+(* This file is distributed under the terms of the *)
+(* GNU Lesser General Public License Version 2.1 *)
+(*************************************************************)
+(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *)
+(*************************************************************)
+*/
+
+#include "gmp.h"
+#include "certif.h"
+
+#ifndef __FACTORIZE_H__
+
+void set_verbose();
+pock_certif_t mersenne_certif (mpz_t t, unsigned long int p);
+pock_certif_t pock_certif (mpz_t t);
+void extend_lc (certif_t lc, pock_certif_t c, unsigned long int min,
+ unsigned long int max );
+#define __FACTORIZE_H__
+#endif /* __FACTORIZE_H__ */