Hiding tactic value representations.

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

1 files changed, 3 insertions, 3 deletions

diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 5556912ebb..03d7c645e4 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -193,9 +193,9 @@ let exec_tactic env n f args =
     Tacinterp.eval_tactic(ltac_call f (args@[getter])) (dummy_goal env) in
   !res
 
-let constr_of = function
-  | VConstr ([],c) -> c
-  | _ -> failwith "Ring.exec_tactic: anomaly"
+let constr_of v = match Value.to_constr v with
+  | Some c -> c
+  | None -> failwith "Ring.exec_tactic: anomaly"
 
 let stdlib_modules =
   [["Coq";"Setoids";"Setoid"];