aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--dev/top_printers.ml3
-rw-r--r--grammar/argextend.ml432
-rw-r--r--grammar/q_coqast.ml43
-rw-r--r--grammar/tacextend.ml438
-rw-r--r--lib/genarg.ml33
-rw-r--r--lib/genarg.mli16
-rw-r--r--parsing/pcoq.ml410
-rw-r--r--plugins/setoid_ring/newring.ml44
-rw-r--r--printing/pptactic.ml21
-rw-r--r--tactics/taccoerce.ml7
-rw-r--r--tactics/tacintern.ml3
-rw-r--r--tactics/tacinterp.ml86
-rw-r--r--tactics/tacsubst.ml3
13 files changed, 97 insertions, 162 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 9d6b4886b..6d90af997 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -366,8 +366,7 @@ let rec pr_argument_type = function
| ConstrWithBindingsArgType -> str"constr-with-bindings"
| BindingsArgType -> str"bindings"
| RedExprArgType -> str"redexp"
- | List0ArgType t -> pr_argument_type t ++ str" list0"
- | List1ArgType t -> pr_argument_type t ++ str" list1"
+ | ListArgType t -> pr_argument_type t ++ str" list"
| OptArgType t -> pr_argument_type t ++ str" opt"
| PairArgType (t1,t2) ->
str"("++ pr_argument_type t1 ++ str"*" ++ pr_argument_type t2 ++str")"
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index dfcaa4e84..d8f615a98 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -12,6 +12,7 @@ open Genarg
open Q_util
open Egramml
open Compat
+open Pcoq
let loc = CompatLoc.ghost
let default_loc = <:expr< Loc.ghost >>
@@ -42,8 +43,7 @@ let rec make_wit loc = function
| OpenConstrArgType b -> <:expr< Constrarg.wit_open_constr_gen $mlexpr_of_bool b$ >>
| ConstrWithBindingsArgType -> <:expr< Constrarg.wit_constr_with_bindings >>
| BindingsArgType -> <:expr< Constrarg.wit_bindings >>
- | List0ArgType t -> <:expr< Genarg.wit_list0 $make_wit loc t$ >>
- | List1ArgType t -> <:expr< Genarg.wit_list1 $make_wit loc t$ >>
+ | ListArgType t -> <:expr< Genarg.wit_list $make_wit loc t$ >>
| OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >>
| PairArgType (t1,t2) ->
<:expr< Genarg.wit_pair $make_wit loc t1$ $make_wit loc t2$ >>
@@ -56,16 +56,26 @@ let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >>
let has_extraarg =
List.exists (function GramNonTerminal(_,ExtraArgType _,_,_) -> true | _ -> false)
+let rec is_possibly_empty = function
+| Aopt _ | Alist0 _ | Alist0sep _ | Amodifiers _ -> true
+| Alist1 t | Alist1sep (t, _) -> is_possibly_empty t
+| _ -> false
+
+let rec get_empty_entry = function
+| Aopt _ -> <:expr< None >>
+| Alist0 _ | Alist0sep _ | Amodifiers _ -> <:expr< [] >>
+| Alist1 t | Alist1sep (t, _) -> <:expr< [$get_empty_entry t$] >>
+| _ -> assert false
+
let statically_known_possibly_empty s (prods,_) =
List.for_all (function
| GramNonTerminal(_,ExtraArgType s',_,_) ->
(* For ExtraArg we don't know (we'll have to test dynamically) *)
(* unless it is a recursive call *)
s <> s'
- | GramNonTerminal(_,(OptArgType _|List0ArgType _),_,_) ->
- (* Opt and List0 parses the empty string *)
- true
- | _ ->
+ | GramNonTerminal(_,_,e,_) ->
+ is_possibly_empty e
+ | GramTerminal _ ->
(* This consumes a token for sure *) false)
prods
@@ -76,10 +86,8 @@ let possibly_empty_subentries loc (prods,act) =
let s = Names.Id.to_string id in <:expr< let $lid:s$ = $v$ in $e$ >> in
let rec aux = function
| [] -> <:expr< let loc = $default_loc$ in let _ = loc in $act$ >>
- | GramNonTerminal(_,OptArgType _,_,p) :: tl ->
- bind_name p <:expr< None >> (aux tl)
- | GramNonTerminal(_,List0ArgType _,_,p) :: tl ->
- bind_name p <:expr< [] >> (aux tl)
+ | GramNonTerminal(_,_,e,p) :: tl when is_possibly_empty e ->
+ bind_name p (get_empty_entry e) (aux tl)
| GramNonTerminal(_,(ExtraArgType _ as t),_,p) :: tl ->
(* We check at runtime if extraarg s parses "epsilon" *)
let s = match p with None -> "_" | Some id -> Names.Id.to_string id in
@@ -93,7 +101,7 @@ let possibly_empty_subentries loc (prods,act) =
(* declares loc because some code can refer to it; *)
(* ensures loc is used to avoid "unused variable" warning *)
(true, <:expr< try Some $aux prods$
- with [ e when Errors.noncritical e -> None ] >>)
+ with [ Exit -> None ] >>)
else
(* Static optimisation *)
(false, aux prods)
@@ -262,7 +270,7 @@ EXTEND
[ "2"
[ e1 = argtype; "*"; e2 = argtype -> PairArgType (e1, e2) ]
| "1"
- [ e = argtype; LIDENT "list" -> List0ArgType e
+ [ e = argtype; LIDENT "list" -> ListArgType e
| e = argtype; LIDENT "option" -> OptArgType e ]
| "0"
[ e = LIDENT -> fst (interp_entry_name false None e "")
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index acb6c8347..9e8ff8b64 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -214,8 +214,7 @@ let rec mlexpr_of_argtype loc = function
| Genarg.SortArgType -> <:expr< Genarg.SortArgType >>
| Genarg.ConstrArgType -> <:expr< Genarg.ConstrArgType >>
| Genarg.ConstrMayEvalArgType -> <:expr< Genarg.ConstrMayEvalArgType >>
- | Genarg.List0ArgType t -> <:expr< Genarg.List0ArgType $mlexpr_of_argtype loc t$ >>
- | Genarg.List1ArgType t -> <:expr< Genarg.List1ArgType $mlexpr_of_argtype loc t$ >>
+ | Genarg.ListArgType t -> <:expr< Genarg.ListArgType $mlexpr_of_argtype loc t$ >>
| Genarg.OptArgType t -> <:expr< Genarg.OptArgType $mlexpr_of_argtype loc t$ >>
| Genarg.PairArgType (t1,t2) ->
let t1 = mlexpr_of_argtype loc t1 in
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index d494a92d8..6e241cf87 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -111,6 +111,26 @@ let make_one_printing_rule se (pt,e) =
let make_printing_rule se = mlexpr_of_list (make_one_printing_rule se)
+let make_empty_check = function
+| GramNonTerminal(_, t, e, _)->
+ let is_extra = match t with ExtraArgType _ -> true | _ -> false in
+ if is_possibly_empty e || is_extra then
+ (* This possibly parses epsilon *)
+ let wit = make_wit loc t in
+ let rawwit = make_rawwit loc t in
+ <:expr<
+ match Genarg.default_empty_value $wit$ with
+ [ None -> raise Exit
+ | Some v ->
+ Tacintern.intern_genarg Tacintern.fully_empty_glob_sign
+ (Genarg.in_gen $rawwit$ v) ] >>
+ else
+ (* This does not parse epsilon (this Exit is static time) *)
+ raise Exit
+| GramTerminal _ ->
+ (* Idem *)
+ raise Exit
+
let rec possibly_empty_subentries loc = function
| [] -> []
| (s,prodsl) :: l ->
@@ -118,24 +138,10 @@ let rec possibly_empty_subentries loc = function
| [] -> (false,<:expr< None >>)
| prods :: rest ->
try
- let l = List.map (function
- | GramNonTerminal(_,(List0ArgType _|
- OptArgType _|
- ExtraArgType _ as t),_,_)->
- (* This possibly parses epsilon *)
- let wit = make_wit loc t in
- let rawwit = make_rawwit loc t in
- <:expr< match Genarg.default_empty_value $wit$ with
- [ None -> failwith ""
- | Some v ->
- Tacintern.intern_genarg Tacintern.fully_empty_glob_sign
- (Genarg.in_gen $rawwit$ v) ] >>
- | GramTerminal _ | GramNonTerminal(_,_,_,_) ->
- (* This does not parse epsilon (this Exit is static time) *)
- raise Exit) prods in
+ let l = List.map make_empty_check prods in
if has_extraarg prods then
(true,<:expr< try Some $mlexpr_of_list (fun x -> x) l$
- with [ Failure "" -> $snd (aux rest)$ ] >>)
+ with [ Exit -> $snd (aux rest)$ ] >>)
else
(true, <:expr< Some $mlexpr_of_list (fun x -> x) l$ >>)
with Exit -> aux rest in
diff --git a/lib/genarg.ml b/lib/genarg.ml
index c201d78b4..358a010ae 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -25,8 +25,7 @@ type argument_type =
| ConstrWithBindingsArgType
| BindingsArgType
| RedExprArgType
- | List0ArgType of argument_type
- | List1ArgType of argument_type
+ | ListArgType of argument_type
| OptArgType of argument_type
| PairArgType of argument_type * argument_type
| ExtraArgType of string
@@ -45,8 +44,7 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
| ConstrWithBindingsArgType, ConstrWithBindingsArgType -> true
| BindingsArgType, BindingsArgType -> true
| RedExprArgType, RedExprArgType -> true
-| List0ArgType arg1, List0ArgType arg2 -> argument_type_eq arg1 arg2
-| List1ArgType arg1, List1ArgType arg2 -> argument_type_eq arg1 arg2
+| ListArgType arg1, ListArgType arg2 -> argument_type_eq arg1 arg2
| OptArgType arg1, OptArgType arg2 -> argument_type_eq arg1 arg2
| PairArgType (arg1l, arg1r), PairArgType (arg2l, arg2r) ->
argument_type_eq arg1l arg2l && argument_type_eq arg1r arg2r
@@ -73,9 +71,7 @@ let rawwit t = t
let glbwit t = t
let topwit t = t
-let wit_list0 t = List0ArgType t
-
-let wit_list1 t = List1ArgType t
+let wit_list t = ListArgType t
let wit_opt t = OptArgType t
@@ -85,15 +81,10 @@ let in_gen t o = (t,Obj.repr o)
let out_gen t (t',o) = if argument_type_eq t t' then Obj.magic o else failwith "out_gen"
let genarg_tag (s,_) = s
-let fold_list0 f = function
- | (List0ArgType t, l) ->
- List.fold_right (fun x -> f (in_gen t x)) (Obj.magic l)
- | _ -> failwith "Genarg: not a list0"
-
-let fold_list1 f = function
- | (List1ArgType t, l) ->
+let fold_list f = function
+ | (ListArgType t, l) ->
List.fold_right (fun x -> f (in_gen t x)) (Obj.magic l)
- | _ -> failwith "Genarg: not a list1"
+ | _ -> failwith "Genarg: not a list"
let fold_opt f a = function
| (OptArgType t, l) ->
@@ -108,18 +99,12 @@ let fold_pair f = function
f (in_gen t1 x1) (in_gen t2 x2)
| _ -> failwith "Genarg: not a pair"
-let app_list0 f = function
- | (List0ArgType t as u, l) ->
+let app_list f = function
+ | (ListArgType t as u, l) ->
let o = Obj.magic l in
(u, Obj.repr (List.map (fun x -> out_gen t (f (in_gen t x))) o))
| _ -> failwith "Genarg: not a list0"
-let app_list1 f = function
- | (List1ArgType t as u, l) ->
- let o = Obj.magic l in
- (u, Obj.repr (List.map (fun x -> out_gen t (f (in_gen t x))) o))
- | _ -> failwith "Genarg: not a list1"
-
let app_opt f = function
| (OptArgType t as u, l) ->
let o = Obj.magic l in
@@ -175,7 +160,7 @@ let make0 = create_arg
let default_empty_value t =
let rec aux = function
- | List0ArgType _ -> Some (Obj.repr [])
+ | ListArgType _ -> Some (Obj.repr [])
| OptArgType _ -> Some (Obj.repr None)
| PairArgType(t1, t2) ->
(match aux t1, aux t2 with
diff --git a/lib/genarg.mli b/lib/genarg.mli
index 8152a19ed..a7232c6bd 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -162,10 +162,7 @@ val top_unpack : 'r top_unpack -> tlevel generic_argument -> 'r
Those functions fail if they are applied to an argument which has not the right
dynamic type. *)
-val fold_list0 :
- ('a generic_argument -> 'c -> 'c) -> 'a generic_argument -> 'c -> 'c
-
-val fold_list1 :
+val fold_list :
('a generic_argument -> 'c -> 'c) -> 'a generic_argument -> 'c -> 'c
val fold_opt :
@@ -178,10 +175,7 @@ val fold_pair :
(** [app_list0] fails if applied to an argument not of tag [List0 t]
for some [t]; it's the responsability of the caller to ensure it *)
-val app_list0 : ('a generic_argument -> 'b generic_argument) ->
-'a generic_argument -> 'b generic_argument
-
-val app_list1 : ('a generic_argument -> 'b generic_argument) ->
+val app_list : ('a generic_argument -> 'b generic_argument) ->
'a generic_argument -> 'b generic_argument
val app_opt : ('a generic_argument -> 'b generic_argument) ->
@@ -210,8 +204,7 @@ type argument_type =
| ConstrWithBindingsArgType
| BindingsArgType
| RedExprArgType
- | List0ArgType of argument_type
- | List1ArgType of argument_type
+ | ListArgType of argument_type
| OptArgType of argument_type
| PairArgType of argument_type * argument_type
| ExtraArgType of string
@@ -250,8 +243,7 @@ end
(** {6 Parameterized types} *)
-val wit_list0 : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
-val wit_list1 : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
+val wit_list : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
val wit_opt : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type
val wit_pair : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type ->
('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 211bf2632..d74de5ac6 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -768,23 +768,23 @@ let rec interp_entry_name static up_level s sep =
let l = String.length s in
if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
let t, g = interp_entry_name static up_level (String.sub s 3 (l-8)) "" in
- List1ArgType t, Alist1 g
+ ListArgType t, Alist1 g
else if l > 12 && coincide s "ne_" 0 &&
coincide s "_list_sep" (l-9) then
let t, g = interp_entry_name static up_level (String.sub s 3 (l-12)) "" in
- List1ArgType t, Alist1sep (g,sep)
+ ListArgType t, Alist1sep (g,sep)
else if l > 5 && coincide s "_list" (l-5) then
let t, g = interp_entry_name static up_level (String.sub s 0 (l-5)) "" in
- List0ArgType t, Alist0 g
+ ListArgType t, Alist0 g
else if l > 9 && coincide s "_list_sep" (l-9) then
let t, g = interp_entry_name static up_level (String.sub s 0 (l-9)) "" in
- List0ArgType t, Alist0sep (g,sep)
+ ListArgType t, Alist0sep (g,sep)
else if l > 4 && coincide s "_opt" (l-4) then
let t, g = interp_entry_name static up_level (String.sub s 0 (l-4)) "" in
OptArgType t, Aopt g
else if l > 5 && coincide s "_mods" (l-5) then
let t, g = interp_entry_name static up_level (String.sub s 0 (l-1)) "" in
- List0ArgType t, Amodifiers g
+ ListArgType t, Amodifiers g
else
let s = match s with "hyp" -> "var" | _ -> s in
let check_lvl n = match up_level with
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 388431a62..aecbbfe85 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -123,14 +123,14 @@ let closed_term_ast l =
TacFun([Some(Id.of_string"t")],
TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term",
[Genarg.in_gen Constrarg.wit_constr (mkVar(Id.of_string"t"));
- Genarg.in_gen (Genarg.wit_list1 Constrarg.wit_ref) l])))
+ Genarg.in_gen (Genarg.wit_list Constrarg.wit_ref) l])))
*)
let closed_term_ast l =
let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in
TacFun([Some(Id.of_string"t")],
TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term",
[Genarg.in_gen (Genarg.glbwit Constrarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None);
- Genarg.in_gen (Genarg.glbwit (Genarg.wit_list1 Constrarg.wit_ref)) l])))
+ Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Constrarg.wit_ref)) l])))
(*
let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
*)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 0fd3b454c..04a2ca1e3 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -161,12 +161,9 @@ let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generi
pr_with_bindings prc prlc (out_gen (rawwit wit_constr_with_bindings) x)
| BindingsArgType ->
pr_bindings_no_with prc prlc (out_gen (rawwit wit_bindings) x)
- | List0ArgType _ ->
+ | ListArgType _ ->
hov 0 (pr_sequence (pr_raw_generic prc prlc prtac prpat prref)
- (fold_list0 (fun a l -> a::l) x []))
- | List1ArgType _ ->
- hov 0 (pr_sequence (pr_raw_generic prc prlc prtac prpat prref)
- (fold_list1 (fun a l -> a::l) x []))
+ (fold_list (fun a l -> a::l) x []))
| OptArgType _ -> hov 0 (fold_opt (pr_raw_generic prc prlc prtac prpat prref) (mt()) x)
| PairArgType _ ->
hov 0
@@ -203,12 +200,9 @@ let rec pr_glb_generic prc prlc prtac prpat x =
pr_with_bindings prc prlc (out_gen (glbwit wit_constr_with_bindings) x)
| BindingsArgType ->
pr_bindings_no_with prc prlc (out_gen (glbwit wit_bindings) x)
- | List0ArgType _ ->
- hov 0 (pr_sequence (pr_glb_generic prc prlc prtac prpat)
- (fold_list0 (fun a l -> a::l) x []))
- | List1ArgType _ ->
+ | ListArgType _ ->
hov 0 (pr_sequence (pr_glb_generic prc prlc prtac prpat)
- (fold_list1 (fun a l -> a::l) x []))
+ (fold_list (fun a l -> a::l) x []))
| OptArgType _ -> hov 0 (fold_opt (pr_glb_generic prc prlc prtac prpat) (mt()) x)
| PairArgType _ ->
hov 0
@@ -239,12 +233,9 @@ let rec pr_top_generic prc prlc prtac prpat x =
pr_with_bindings prc prlc (c,b)
| BindingsArgType ->
pr_bindings_no_with prc prlc (out_gen (topwit wit_bindings) x).Evd.it
- | List0ArgType _ ->
- hov 0 (pr_sequence (pr_top_generic prc prlc prtac prpat)
- (fold_list0 (fun a l -> a::l) x []))
- | List1ArgType _ ->
+ | ListArgType _ ->
hov 0 (pr_sequence (pr_top_generic prc prlc prtac prpat)
- (fold_list1 (fun a l -> a::l) x []))
+ (fold_list (fun a l -> a::l) x []))
| OptArgType _ -> hov 0 (fold_opt (pr_top_generic prc prlc prtac prpat) (mt()) x)
| PairArgType _ ->
hov 0
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index 9318955df..06a9ab811 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -58,11 +58,8 @@ let to_int v =
let to_list v =
let v = normalize v in
- try Some (fold_list0 (fun v accu -> v :: accu) v [])
- with Failure _ ->
- try Some (fold_list1 (fun v accu -> v :: accu) v [])
- with Failure _ ->
- None
+ try Some (fold_list (fun v accu -> v :: accu) v [])
+ with Failure _ -> None
end
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 1a63ca2da..d176c516f 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -789,8 +789,7 @@ and intern_genarg ist x =
| BindingsArgType ->
in_gen (glbwit wit_bindings)
(intern_bindings ist (out_gen (rawwit wit_bindings) x))
- | List0ArgType _ -> app_list0 (intern_genarg ist) x
- | List1ArgType _ -> app_list1 (intern_genarg ist) x
+ | ListArgType _ -> app_list (intern_genarg ist) x
| OptArgType _ -> app_opt (intern_genarg ist) x
| PairArgType _ -> app_pair (intern_genarg ist) (intern_genarg ist) x
| ExtraArgType s ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index d5c48f9e6..dea7cd5a2 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1435,18 +1435,12 @@ and interp_genarg ist gl x =
| BindingsArgType ->
in_gen (topwit wit_bindings)
(pack_sigma (interp_bindings ist (pf_env gl) (project gl) (out_gen (glbwit wit_bindings) x)))
- | List0ArgType ConstrArgType ->
- let (sigma,v) = interp_genarg_constr_list0 ist gl x in
+ | ListArgType ConstrArgType ->
+ let (sigma,v) = interp_genarg_constr_list ist gl x in
evdref := sigma;
v
- | List1ArgType ConstrArgType ->
- let (sigma,v) = interp_genarg_constr_list1 ist gl x in
- evdref := sigma;
- v
- | List0ArgType VarArgType -> interp_genarg_var_list0 ist gl x
- | List1ArgType VarArgType -> interp_genarg_var_list1 ist gl x
- | List0ArgType _ -> app_list0 (interp_genarg ist gl) x
- | List1ArgType _ -> app_list1 (interp_genarg ist gl) x
+ | ListArgType VarArgType -> interp_genarg_var_list ist gl x
+ | ListArgType _ -> app_list (interp_genarg ist gl) x
| OptArgType _ -> app_opt (interp_genarg ist gl) x
| PairArgType _ -> app_pair (interp_genarg ist gl) (interp_genarg ist gl) x
| ExtraArgType s ->
@@ -1457,25 +1451,15 @@ and interp_genarg ist gl x =
let v = interp_genarg ist gl x in
!evdref , v
-and interp_genarg_constr_list0 ist gl x =
- let lc = out_gen (glbwit (wit_list0 wit_constr)) x in
- let (sigma,lc) = pf_apply (interp_constr_list ist) gl lc in
- sigma , in_gen (topwit (wit_list0 wit_constr)) lc
-
-and interp_genarg_constr_list1 ist gl x =
- let lc = out_gen (glbwit (wit_list1 wit_constr)) x in
+and interp_genarg_constr_list ist gl x =
+ let lc = out_gen (glbwit (wit_list wit_constr)) x in
let (sigma,lc) = pf_apply (interp_constr_list ist) gl lc in
- sigma , in_gen (topwit (wit_list1 wit_constr)) lc
+ sigma , in_gen (topwit (wit_list wit_constr)) lc
-and interp_genarg_var_list0 ist gl x =
- let lc = out_gen (glbwit (wit_list0 wit_var)) x in
+and interp_genarg_var_list ist gl x =
+ let lc = out_gen (glbwit (wit_list wit_var)) x in
let lc = interp_hyp_list ist gl lc in
- in_gen (topwit (wit_list0 wit_var)) lc
-
-and interp_genarg_var_list1 ist gl x =
- let lc = out_gen (glbwit (wit_list1 wit_var)) x in
- let lc = interp_hyp_list ist gl lc in
- in_gen (topwit (wit_list1 wit_var)) lc
+ in_gen (topwit (wit_list wit_var)) lc
(* Interprets the Match expressions *)
and interp_match ist g lz constr lmr =
@@ -1909,8 +1893,8 @@ and interp_atomic ist gl tac =
let (sigma,c_interp) = interp_constr_may_eval ist gl (out_gen (glbwit wit_constr_may_eval) x) in
evdref := sigma;
Value.of_constr c_interp
- | List0ArgType ConstrArgType ->
- let wit = glbwit (wit_list0 wit_constr) in
+ | ListArgType ConstrArgType ->
+ let wit = glbwit (wit_list wit_constr) in
let (sigma,l_interp) =
List.fold_right begin fun c (sigma,acc) ->
let (sigma,c_interp) = mk_constr_value ist { gl with sigma=sigma } c in
@@ -1918,45 +1902,21 @@ and interp_atomic ist gl tac =
end (out_gen wit x) (project gl,[])
in
evdref := sigma;
- in_gen (topwit (wit_list0 wit_genarg)) l_interp
- | List0ArgType VarArgType ->
- let wit = glbwit (wit_list0 wit_var) in
- let ans = List.map (mk_hyp_value ist gl) (out_gen wit x) in
- in_gen (topwit (wit_list0 wit_genarg)) ans
- | List0ArgType IntOrVarArgType ->
- let wit = glbwit (wit_list0 wit_int_or_var) in
- let ans = List.map (mk_int_or_var_value ist) (out_gen wit x) in
- in_gen (topwit (wit_list0 wit_genarg)) ans
- | List0ArgType (IdentArgType b) ->
- let wit = glbwit (wit_list0 (wit_ident_gen b)) in
- let mk_ident x = value_of_ident (interp_fresh_ident ist env x) in
- let ans = List.map mk_ident (out_gen wit x) in
- in_gen (topwit (wit_list0 wit_genarg)) ans
- | List1ArgType ConstrArgType ->
- let wit = glbwit (wit_list1 wit_constr) in
- let (sigma, l_interp) =
- List.fold_right begin fun c (sigma,acc) ->
- let (sigma,c_interp) = mk_constr_value ist { gl with sigma=sigma } c in
- sigma , c_interp::acc
- end (out_gen wit x) (project gl,[])
- in
- evdref:=sigma;
- in_gen (topwit (wit_list1 wit_genarg)) l_interp
- | List1ArgType VarArgType ->
- let wit = glbwit (wit_list1 wit_var) in
+ in_gen (topwit (wit_list wit_genarg)) l_interp
+ | ListArgType VarArgType ->
+ let wit = glbwit (wit_list wit_var) in
let ans = List.map (mk_hyp_value ist gl) (out_gen wit x) in
- in_gen (topwit (wit_list1 wit_genarg)) ans
- | List1ArgType IntOrVarArgType ->
- let wit = glbwit (wit_list1 wit_int_or_var) in
+ in_gen (topwit (wit_list wit_genarg)) ans
+ | ListArgType IntOrVarArgType ->
+ let wit = glbwit (wit_list wit_int_or_var) in
let ans = List.map (mk_int_or_var_value ist) (out_gen wit x) in
- in_gen (topwit (wit_list1 wit_genarg)) ans
- | List1ArgType (IdentArgType b) ->
- let wit = glbwit (wit_list1 (wit_ident_gen b)) in
+ in_gen (topwit (wit_list wit_genarg)) ans
+ | ListArgType (IdentArgType b) ->
+ let wit = glbwit (wit_list (wit_ident_gen b)) in
let mk_ident x = value_of_ident (interp_fresh_ident ist env x) in
let ans = List.map mk_ident (out_gen wit x) in
- in_gen (topwit (wit_list1 wit_genarg)) ans
- | List0ArgType _ -> app_list0 f x
- | List1ArgType _ -> app_list1 f x
+ in_gen (topwit (wit_list wit_genarg)) ans
+ | ListArgType _ -> app_list f x
| ExtraArgType _ ->
(** Special treatment of tactics *)
let gl = { gl with sigma = !evdref } in
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 11b747e72..80a563322 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -317,8 +317,7 @@ and subst_genarg subst (x:glob_generic_argument) =
| BindingsArgType ->
in_gen (glbwit wit_bindings)
(subst_bindings subst (out_gen (glbwit wit_bindings) x))
- | List0ArgType _ -> app_list0 (subst_genarg subst) x
- | List1ArgType _ -> app_list1 (subst_genarg subst) x
+ | ListArgType _ -> app_list (subst_genarg subst) x
| OptArgType _ -> app_opt (subst_genarg subst) x
| PairArgType _ -> app_pair (subst_genarg subst) (subst_genarg subst) x
| ExtraArgType s ->