From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 25 Jul 2008 15:12:53 +0200
Subject: Imported Upstream version 8.2~beta3+dfsg

---
 interp/genarg.ml | 26 +++++++++++++++++---------
 1 file changed, 17 insertions(+), 9 deletions(-)

(limited to 'interp/genarg.ml')

diff --git a/interp/genarg.ml b/interp/genarg.ml
index 77ed1fe6..49c157f2 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: genarg.ml 8926 2006-06-08 20:23:17Z herbelin $ *)
+(* $Id: genarg.ml 10753 2008-04-04 14:55:47Z herbelin $ *)
 
 open Pp
 open Util
@@ -16,6 +16,7 @@ open Nametab
 open Rawterm
 open Topconstr
 open Term
+open Evd
 
 type argument_type =
   (* Basic types *)
@@ -44,19 +45,25 @@ type argument_type =
   | ExtraArgType of string
 
 type 'a and_short_name = 'a * identifier located option
+type 'a or_by_notation = AN of 'a | ByNotation of loc * string
+
 type rawconstr_and_expr = rawconstr * constr_expr option
+type open_constr_expr = unit * constr_expr
+type open_rawconstr = unit * rawconstr_and_expr
+
+type 'a with_ebindings = 'a * open_constr bindings
 
 (* Dynamics but tagged by a type expression *)
 
-type ('a,'b) generic_argument = argument_type * Obj.t
+type 'a generic_argument = argument_type * Obj.t
 
 let dyntab = ref ([] : string list)
 
 type rlevel = constr_expr
 type glevel = rawconstr_and_expr
-type tlevel = constr
+type tlevel = open_constr
 
-type ('a,'b,'c) abstract_argument_type = argument_type
+type ('a,'b) abstract_argument_type = argument_type
 
 let create_arg s =
   if List.mem s !dyntab then
@@ -72,6 +79,8 @@ type intro_pattern_expr =
   | IntroWildcard
   | IntroIdentifier of identifier
   | IntroAnonymous
+  | IntroRewrite of bool
+  | IntroFresh of identifier
 and case_intro_pattern_expr = intro_pattern_expr list list
 
 let rec pr_intro_pattern = function
@@ -79,6 +88,9 @@ let rec pr_intro_pattern = function
   | IntroWildcard -> str "_"
   | IntroIdentifier id -> pr_id id
   | IntroAnonymous -> str "?"
+  | IntroRewrite true -> str "->"
+  | IntroRewrite false -> str "<-"
+  | IntroFresh id -> str "?" ++ pr_id id
 
 and pr_case_intro_pattern = function
   | [pl] ->
@@ -88,10 +100,6 @@ and pr_case_intro_pattern = function
       hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
       ++ str "]"
 
-type open_constr = Evd.evar_map * Term.constr
-type open_constr_expr = unit * constr_expr
-type open_rawconstr = unit * rawconstr_and_expr
-
 let rawwit_bool = BoolArgType
 let globwit_bool = BoolArgType
 let wit_bool = BoolArgType
@@ -218,7 +226,7 @@ let app_list1 f = function
 let app_opt f = function
   | (OptArgType t as u, l) ->
       let o = Obj.magic l in
-      (u, Obj.repr (option_map (fun x -> out_gen t (f (in_gen t x))) o))
+      (u, Obj.repr (Option.map (fun x -> out_gen t (f (in_gen t x))) o))
   | _ -> failwith "Genarg: not an opt"
 
 let app_pair f1 f2 = function
-- 
cgit v1.2.3