git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13338 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 3 insertions, 7 deletions

diff --git a/plugins/nsatz/Nsatz_domain.v b/plugins/nsatz/Nsatz_domain.v
index ee430becf..7da698db5 100644
--- a/plugins/nsatz/Nsatz_domain.v
+++ b/plugins/nsatz/Nsatz_domain.v
@@ -7,13 +7,9 @@
 (************************************************************************)
 
 (*
- Tactic nsatz: proofs of polynomials equalities with variables in R.
- Uses Hilbert Nullstellensatz and Buchberger algorithm.
- Thanks to B.Gregoire for the verification of the certicate
- and L.Thery for help on ring tactic, 
- and to B.Barras for modularization of the ocaml code.
- Example: see test-suite/success/Nsatz.v
- L.Pottier, june 2010
+ Tactic nsatz: proofs of polynomials equalities in a domain (ring without zero divisor).
+ Reification is done by type classes.
+ Example: see test-suite/success/Nsatz_domain.v
 *)
 
 Require Import List.