Rewrite API using EConstr.

2 files changed, 30 insertions, 6 deletions

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 54206aa955..5de2c41517 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -382,6 +382,9 @@ let enstack_subsubgoals env se stack gls=
 	    Array.iteri process gentypes
       | _ -> ()
 
+let nf_meta sigma c =
+  EConstr.Unsafe.to_constr (Reductionops.nf_meta sigma (EConstr.of_constr c))
+
 let rec nf_list evd =
   function
       [] -> []
@@ -389,7 +392,7 @@ let rec nf_list evd =
 	if meta_defined evd m then
 	    nf_list evd others
 	else
-	  (m,Reductionops.nf_meta evd typ)::nf_list evd others
+	  (m,nf_meta evd typ)::nf_list evd others
 
 let find_subsubgoal c ctyp skip submetas gls =
   let env= pf_env gls in
@@ -424,7 +427,7 @@ let find_subsubgoal c ctyp skip submetas gls =
 	  dfs n
 	end in
   let nse= try dfs skip with Stack.Empty -> raise Not_found in
-    nf_list nse.se_evd nse.se_meta_list,Reductionops.nf_meta nse.se_evd (mkMeta 0)
+    nf_list nse.se_evd nse.se_meta_list,nf_meta nse.se_evd (mkMeta 0)
 
 let concl_refiner metas body gls =
   let concl = pf_concl gls in
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 089e76d7a0..4492b854b4 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -416,11 +416,18 @@ let theory_to_obj : ring_info -> obj =
 
 
 let setoid_of_relation env evd a r =
+  let a = EConstr.of_constr a in
+  let r = EConstr.of_constr r in
   try
     let evm = !evd in
     let evm, refl = Rewrite.get_reflexive_proof env evm a r in
     let evm, sym = Rewrite.get_symmetric_proof env evm a r in
     let evm, trans = Rewrite.get_transitive_proof env evm a r in
+    let refl = EConstr.Unsafe.to_constr refl in
+    let sym = EConstr.Unsafe.to_constr sym in
+    let trans = EConstr.Unsafe.to_constr trans in
+    let a = EConstr.Unsafe.to_constr a in
+    let r = EConstr.Unsafe.to_constr r in
       evd := evm;
       lapp coq_mk_Setoid [|a ; r ; refl; sym; trans |]
   with Not_found ->
@@ -498,22 +505,32 @@ let ring_equality env evd (r,add,mul,opp,req) =
 	  (setoid,op_morph)
     | _ ->
 	let setoid = setoid_of_relation (Global.env ()) evd r req in
-	let signature = [Some (r,Some req);Some (r,Some req)],Some(r,Some req) in
+	let signature =
+          let r = EConstr.of_constr r in
+          let req = EConstr.of_constr req in
+          [Some (r,Some req);Some (r,Some req)],Some(r,Some req)
+        in
+(* 	let signature = [Some (r,Some req);Some (r,Some req)],Some(r,Some req) in *)
 	let add_m, add_m_lem =
-	  try Rewrite.default_morphism signature add
+	  try Rewrite.default_morphism signature (EConstr.of_constr add)
           with Not_found ->
             error "ring addition should be declared as a morphism" in
+        let add_m_lem = EConstr.Unsafe.to_constr add_m_lem in
 	let mul_m, mul_m_lem =
-          try Rewrite.default_morphism signature mul
+          try Rewrite.default_morphism signature (EConstr.of_constr mul)
           with Not_found ->
             error "ring multiplication should be declared as a morphism" in
+        let mul_m_lem = EConstr.Unsafe.to_constr mul_m_lem in
         let op_morph =
           match opp with
             | Some opp ->
 		(let opp_m,opp_m_lem =
-		  try Rewrite.default_morphism ([Some(r,Some req)],Some(r,Some req)) opp
+                  let r = EConstr.of_constr r in
+                  let req = EConstr.of_constr req in
+		  try Rewrite.default_morphism ([Some(r,Some req)],Some(r,Some req)) (EConstr.of_constr opp)
 		  with Not_found ->
                     error "ring opposite should be declared as a morphism" in
+                let opp_m_lem = EConstr.Unsafe.to_constr opp_m_lem in
 		let op_morph =
 		  op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in
 		  Flags.if_verbose
@@ -895,11 +912,15 @@ let field_equality evd r inv req =
         mkApp(Universes.constr_of_global (Coqlib.build_coq_eq_data()).congr,[|r;r;inv|])
     | _ ->
 	let _setoid = setoid_of_relation (Global.env ()) evd r req in
+        let r = EConstr.of_constr r in
+        let req = EConstr.of_constr req in
 	let signature = [Some (r,Some req)],Some(r,Some req) in
+	let inv = EConstr.of_constr inv in
 	let inv_m, inv_m_lem =
 	  try Rewrite.default_morphism signature inv
           with Not_found ->
             error "field inverse should be declared as a morphism" in
+        let inv_m_lem = EConstr.Unsafe.to_constr inv_m_lem in
 	  inv_m_lem
 
 let add_field_theory name (sigma,fth) eqth morphth cst_tac inj (pre,post) power sign odiv =