From 8a8fd265158fa3fe7eea65b50c3da722e81fa688 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 1 Aug 2017 14:43:30 +0200
Subject: Binding more primitive tactics.

---
 src/tac2core.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/tac2core.ml')

diff --git a/src/tac2core.ml b/src/tac2core.ml
index e0a65dde2d..fef16dcc06 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -325,7 +325,7 @@ let prm_constr_kind : ml_tactic = function
     |])
   | Const (cst, u) ->
     ValBlk (10, [|
-      Value.of_ext Value.val_constant cst;
+      Value.of_constant cst;
       of_instance sigma u;
     |])
   | Ind (ind, u) ->
-- 
cgit v1.2.3