diff options
| author | Maxime Dénès | 2018-12-12 09:57:09 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-12-12 09:57:09 +0100 |
| commit | d87c4c472478fbcb30de6efabc68473ee36849a1 (patch) | |
| tree | 5b4e1cb66298db57b978374422822ffdf2673100 /plugins/nsatz | |
| parent | 850dfbf59f52b0d3dcba237ee2af5ce99fd1bcd2 (diff) | |
| parent | d00472c59d15259b486868c5ccdb50b6e602a548 (diff) | |
Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix comments.
Diffstat (limited to 'plugins/nsatz')
| -rw-r--r-- | plugins/nsatz/ideal.ml | 4 | ||||
| -rw-r--r-- | plugins/nsatz/nsatz.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml index f8fc943713..1825a4d77c 100644 --- a/plugins/nsatz/ideal.ml +++ b/plugins/nsatz/ideal.ml @@ -609,7 +609,7 @@ type current_problem = { exception NotInIdealUpdate of current_problem let test_dans_ideal cur_pb table metadata p lp len0 = - (** Invariant: [lp] is [List.tl (Array.to_list table.allpol)] *) + (* Invariant: [lp] is [List.tl (Array.to_list table.allpol)] *) let (c,r) = reduce2 table cur_pb.cur_poly lp in info (fun () -> "remainder: "^(stringPcut metadata r)); let cur_pb = { @@ -657,7 +657,7 @@ let deg_hom p = | (a,m)::_ -> Monomial.deg m let pbuchf table metadata cur_pb homogeneous (lp, lpc) p = - (** Invariant: [lp] is [List.tl (Array.to_list table.allpol)] *) + (* Invariant: [lp] is [List.tl (Array.to_list table.allpol)] *) sinfo "computation of the Groebner basis"; let () = match table.hmon with | None -> () diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index ef60a23e80..1777418ef6 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -374,7 +374,7 @@ let remove_zeros lci = let m = List.length lci in let u = Array.make m false in let rec utiles k = - (** TODO: Find a more reasonable implementation of this traversal. *) + (* TODO: Find a more reasonable implementation of this traversal. *) if k >= m || u.(k) then () else let () = u.(k) <- true in |