From 648ce5e08f7245f2a775abd1304783c4167e9f2e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 2 Feb 2017 18:24:58 +0100
Subject: Unifying standard "constr_level" names for constructors of
 local_binder_expr.

RawLocal -> CLocal
---
 plugins/ltac/g_obligations.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4
index d286a58708..3e6e2db605 100644
--- a/plugins/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.ml4
@@ -70,7 +70,7 @@ GEXTEND Gram
   Constr.closed_binder:
     [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" ->
 	  let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in
-          [LocalRawAssum ([id], default_binder_kind, typ)]
+          [CLocalAssum ([id], default_binder_kind, typ)]
     ] ];
 
   END
-- 
cgit v1.2.3