From 41494147b4b7c9a33721faf8e0041900a8df9d64 Mon Sep 17 00:00:00 2001 From: pottier Date: Wed, 28 Jul 2010 11:17:04 +0000 Subject: git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13338 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/nsatz/Nsatz_domain.v | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) (limited to 'plugins/nsatz') 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. -- cgit v1.2.3