diff options
| author |  fkirchne <fkirchne@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-05-28 16:40:21 +0000 |
|---|---|---|
| committer | fkirchne <fkirchne@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-05-28 16:40:21 +0000 |
| commit | 4fc5ff31b342253f889db23a3b46482a4c7fa1ca (patch) | |
| tree | 5f617a4a1f48dec952b0ca5674bb719b063b60ba /plugins/micromega/certificate.ml | |
| parent | f9261830d886bf08599921d42539d8651437303f (diff) | |
A little bit of cleanup, and some annotations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13036 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/micromega/certificate.ml')
| -rw-r--r-- | plugins/micromega/certificate.ml | 16 |
1 files changed, 0 insertions, 16 deletions
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 7ddcf35d3..6b18281b8 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -194,9 +194,6 @@ let q_spec = { let r_spec = z_spec - - - let dev_form n_spec p = let rec dev_form p = match p with @@ -219,7 +216,6 @@ let dev_form n_spec p = pow n in dev_form p - let monomial_to_polynomial mn = Monomial.fold (fun v i acc -> @@ -252,13 +248,6 @@ let rec fixpoint f x = if y' = x then y' else fixpoint f y' - - - - - - - let rec_simpl_cone n_spec e = let simpl_cone = Mc.simpl_cone n_spec.zero n_spec.unit n_spec.mult n_spec.eqb in @@ -271,7 +260,6 @@ let rec_simpl_cone n_spec e = | x -> simpl_cone x in rec_simpl_cone e - let simplify_cone n_spec c = fixpoint (rec_simpl_cone n_spec) c type cone_prod = @@ -281,8 +269,6 @@ type cone_prod = | Other of cone and cone = Mc.zWitness - - let factorise_linear_cone c = let rec cone_list c l = @@ -314,8 +300,6 @@ let factorise_linear_cone c = (rebuild_cone (List.sort Pervasives.compare (cone_list c [])) None) - - (* The binding with Fourier might be a bit obsolete -- how does it handle equalities ? *) |