summaryrefslogtreecommitdiff
path: root/contrib/setoid_ring
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
commitcfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch)
treeb7832bd5d412a5a5d69cb36ae2ded62c71124c22 /contrib/setoid_ring
parent113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff)
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'contrib/setoid_ring')
-rw-r--r--contrib/setoid_ring/Ring_base.v1
-rw-r--r--contrib/setoid_ring/Ring_tac.v1
-rw-r--r--contrib/setoid_ring/newring.ml411
3 files changed, 6 insertions, 7 deletions
diff --git a/contrib/setoid_ring/Ring_base.v b/contrib/setoid_ring/Ring_base.v
index 95b037e3..956a15fe 100644
--- a/contrib/setoid_ring/Ring_base.v
+++ b/contrib/setoid_ring/Ring_base.v
@@ -10,7 +10,6 @@
ring tactic. Abstract rings need more theory, depending on
ZArith_base. *)
-Declare ML Module "newring".
Require Export Ring_theory.
Require Export Ring_tac.
Require Import InitialRing.
diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v
index 46d106d3..ad20fa08 100644
--- a/contrib/setoid_ring/Ring_tac.v
+++ b/contrib/setoid_ring/Ring_tac.v
@@ -4,7 +4,6 @@ Require Import BinPos.
Require Import Ring_polynom.
Require Import BinList.
Require Import InitialRing.
-Declare ML Module "newring".
(* adds a definition id' on the normal form of t and an hypothesis id
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index 3d022add..50b7e47b 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(*i $Id: newring.ml4 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: newring.ml4 11800 2009-01-18 18:34:15Z msozeau $ i*)
open Pp
open Util
@@ -19,12 +19,12 @@ open Environ
open Libnames
open Tactics
open Rawterm
+open Termops
open Tacticals
open Tacexpr
open Pcoq
open Tactic
open Constr
-open Setoid_replace
open Proof_type
open Coqlib
open Tacmach
@@ -452,12 +452,13 @@ let (theory_to_obj, obj_to_theory) =
let setoid_of_relation env a r =
+ let evm = Evd.empty in
try
lapp coq_mk_Setoid
[|a ; r ;
- Class_tactics.reflexive_proof env a r ;
- Class_tactics.symmetric_proof env a r ;
- Class_tactics.transitive_proof env a r |]
+ Class_tactics.get_reflexive_proof env evm a r ;
+ Class_tactics.get_symmetric_proof env evm a r ;
+ Class_tactics.get_transitive_proof env evm a r |]
with Not_found ->
error "cannot find setoid relation"