diff options
| -rw-r--r-- | dev/top_printers.ml | 3 | ||||
| -rw-r--r-- | grammar/argextend.ml4 | 32 | ||||
| -rw-r--r-- | grammar/q_coqast.ml4 | 3 | ||||
| -rw-r--r-- | grammar/tacextend.ml4 | 38 | ||||
| -rw-r--r-- | lib/genarg.ml | 33 | ||||
| -rw-r--r-- | lib/genarg.mli | 16 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 10 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.ml4 | 4 | ||||
| -rw-r--r-- | printing/pptactic.ml | 21 | ||||
| -rw-r--r-- | tactics/taccoerce.ml | 7 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 3 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 86 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 3 |
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 -> |