Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 37 insertions, 1 deletions

diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4
index b3f5393c..07b23972 100644
--- a/parsing/q_util.ml4
+++ b/parsing/q_util.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: q_util.ml4,v 1.2.2.2 2004/07/16 19:30:41 herbelin Exp $ *)
+(* $Id: q_util.ml4 7732 2005-12-26 13:51:24Z herbelin $ *)
 
 (* This file defines standard combinators to build ml expressions *)
 
@@ -66,3 +66,39 @@ let mlexpr_of_string s = <:expr< $str:s$ >>
 let mlexpr_of_option f = function
   | None -> <:expr< None >>
   | Some e -> <:expr< Some $f e$ >>
+
+open Vernacexpr
+open Pcoq
+open Genarg
+
+let rec interp_entry_name loc s =
+  let l = String.length s in
+  if l > 8 & String.sub s 0 3 = "ne_" & String.sub s (l-5) 5 = "_list" then
+    let t, g = interp_entry_name loc (String.sub s 3 (l-8)) in
+    List1ArgType t, <:expr< Gramext.Slist1 $g$ >>
+  else if l > 5 & String.sub s (l-5) 5 = "_list" then
+    let t, g = interp_entry_name loc (String.sub s 0 (l-5)) in
+    List0ArgType t, <:expr< Gramext.Slist0 $g$ >>
+  else if l > 4 & String.sub s (l-4) 4 = "_opt" then
+    let t, g = interp_entry_name loc (String.sub s 0 (l-4)) in
+    OptArgType t, <:expr< Gramext.Sopt $g$ >>
+  else
+    let s = if s = "hyp" then "var" else s in
+    let t, se =
+      match Pcoq.entry_type (Pcoq.get_univ "prim") s with
+	| Some _ as x -> x, <:expr< Prim. $lid:s$ >>
+	| None -> 
+      match Pcoq.entry_type (Pcoq.get_univ "constr") s with
+	| Some _ as x -> x, <:expr< Constr. $lid:s$ >>
+	| None -> 
+      match Pcoq.entry_type (Pcoq.get_univ "tactic") s with
+	| Some _ as x -> x, <:expr< Tactic. $lid:s$ >>
+	| None -> None, <:expr< $lid:s$ >> in
+    let t =
+      match t with
+	| Some t -> t
+	| None ->
+(*	    Pp.warning_with Pp_control.err_ft
+            ("Unknown primitive grammar entry: "^s);*)
+	    ExtraArgType s
+    in t, <:expr< Gramext.Snterm (Pcoq.Gram.Entry.obj $se$) >>