From af1947ae57d0fa6f35a61b86ea9e73e66f2f5fd8 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Mon, 10 Jun 2013 16:25:06 +0000
Subject: Hiding tactic value representations.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16570 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/setoid_ring/newring.ml4 | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins')

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"];
-- 
cgit v1.2.3