From 5cbeafc8d8a7fdf403b864c16ba9c4e7013b0d11 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 5 Aug 2014 12:15:32 +0200
Subject: Small refactoring: use [uconstr] instead of [constr] when relevant in
 grammar rules.

---
 parsing/g_ltac.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 2d9cd3cd41..ea38358660 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -143,12 +143,12 @@ GEXTEND Gram
   ;
   (* Can be used as argument and at toplevel in tactic expressions. *)
   tactic_top_or_arg:
-    [ [ IDENT "uconstr"; ":" ; c = Constr.constr -> UConstr c
+    [ [ IDENT "uconstr"; ":" ; c = uconstr -> UConstr c
       | IDENT "ipattern"; ":"; ipat = simple_intropattern ->
         TacGeneric (genarg_of_ipattern ipat)
       | c = constr_eval -> ConstrMayEval c
       | IDENT "fresh"; l = LIST0 fresh_id -> TacFreshId l
-      | IDENT "type_term"; c=Constr.constr -> TacPretype c
+      | IDENT "type_term"; c=uconstr -> TacPretype c
       | IDENT "numgoals" -> TacNumgoals ] ]
   ;
   fresh_id:
-- 
cgit v1.2.3