diff options
| -rw-r--r-- | parsing/ppextend.ml | 16 | ||||
| -rw-r--r-- | parsing/ppextend.mli | 8 | ||||
| -rw-r--r-- | printing/ppconstr.ml | 8 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 14 |
4 files changed, 23 insertions, 23 deletions
diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml index bf622e5759..369db81497 100644 --- a/parsing/ppextend.ml +++ b/parsing/ppextend.ml @@ -38,10 +38,10 @@ let ppcmd_of_cut = function | PpBrk(n1,n2) -> brk(n1,n2) type unparsing = - | UnpMetaVar of int * entry_relative_level - | UnpBinderMetaVar of int * entry_relative_level - | UnpListMetaVar of int * entry_relative_level * unparsing list - | UnpBinderListMetaVar of int * bool * unparsing list + | UnpMetaVar of entry_relative_level + | UnpBinderMetaVar of entry_relative_level + | UnpListMetaVar of entry_relative_level * unparsing list + | UnpBinderListMetaVar of bool * unparsing list | UnpTerminal of string | UnpBox of ppbox * unparsing Loc.located list | UnpCut of ppcut @@ -50,10 +50,10 @@ type unparsing_rule = unparsing list * entry_level type extra_unparsing_rules = (string * string) list let rec unparsing_eq unp1 unp2 = match (unp1,unp2) with - | UnpMetaVar (n1,p1), UnpMetaVar (n2,p2) -> n1 = n2 && entry_relative_level_eq p1 p2 - | UnpBinderMetaVar (n1,p1), UnpBinderMetaVar (n2,p2) -> n1 = n2 && entry_relative_level_eq p1 p2 - | UnpListMetaVar (n1,p1,l1), UnpListMetaVar (n2,p2,l2) -> n1 = n2 && entry_relative_level_eq p1 p2 && List.for_all2eq unparsing_eq l1 l2 - | UnpBinderListMetaVar (n1,b1,l1), UnpBinderListMetaVar (n2,b2,l2) -> n1 = n2 && b1 = b2 && List.for_all2eq unparsing_eq l1 l2 + | UnpMetaVar p1, UnpMetaVar p2 -> entry_relative_level_eq p1 p2 + | UnpBinderMetaVar p1, UnpBinderMetaVar p2 -> entry_relative_level_eq p1 p2 + | UnpListMetaVar (p1,l1), UnpListMetaVar (p2,l2) -> entry_relative_level_eq p1 p2 && List.for_all2eq unparsing_eq l1 l2 + | UnpBinderListMetaVar (b1,l1), UnpBinderListMetaVar (b2,l2) -> b1 = b2 && List.for_all2eq unparsing_eq l1 l2 | UnpTerminal s1, UnpTerminal s2 -> String.equal s1 s2 | UnpBox (b1,l1), UnpBox (b2,l2) -> b1 = b2 && List.for_all2eq unparsing_eq (List.map snd l1) (List.map snd l2) | UnpCut p1, UnpCut p2 -> p1 = p2 diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli index 8ea6f31241..346fc83f5f 100644 --- a/parsing/ppextend.mli +++ b/parsing/ppextend.mli @@ -30,10 +30,10 @@ val ppcmd_of_cut : ppcut -> Pp.t (** Declare and look for the printing rule for symbolic notations *) type unparsing = - | UnpMetaVar of int * entry_relative_level - | UnpBinderMetaVar of int * entry_relative_level - | UnpListMetaVar of int * entry_relative_level * unparsing list - | UnpBinderListMetaVar of int * bool * unparsing list + | UnpMetaVar of entry_relative_level + | UnpBinderMetaVar of entry_relative_level + | UnpListMetaVar of entry_relative_level * unparsing list + | UnpBinderListMetaVar of bool * unparsing list | UnpTerminal of string | UnpBox of ppbox * unparsing Loc.located list | UnpCut of ppcut diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 75b3e7d406..c2d760ae08 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -92,22 +92,22 @@ let tag_var = tag Tag.variable let rec aux = function | [] -> mt () - | UnpMetaVar (_, prec) as unp :: l -> + | UnpMetaVar prec as unp :: l -> let c = pop env in let pp2 = aux l in let pp1 = pr prec c in return unp pp1 pp2 - | UnpBinderMetaVar (_, prec) as unp :: l -> + | UnpBinderMetaVar prec as unp :: l -> let c = pop bl in let pp2 = aux l in let pp1 = pr_patt prec c in return unp pp1 pp2 - | UnpListMetaVar (_, prec, sl) as unp :: l -> + | UnpListMetaVar (prec, sl) as unp :: l -> let cl = pop envlist in let pp1 = prlist_with_sep (fun () -> aux sl) (pr prec) cl in let pp2 = aux l in return unp pp1 pp2 - | UnpBinderListMetaVar (_, isopen, sl) as unp :: l -> + | UnpBinderListMetaVar (isopen, sl) as unp :: l -> let cl = pop bll in let pp2 = aux l in let pp1 = pr_binders (fun () -> aux sl) isopen cl in diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index a802fc98a6..8f64500996 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -395,11 +395,11 @@ let unparsing_metavar i from typs = let prec = unparsing_precedence_of_entry_type from x in match x with | ETConstr _ | ETGlobal | ETBigint -> - UnpMetaVar (i,prec) + UnpMetaVar prec | ETPattern _ -> - UnpBinderMetaVar (i,prec) + UnpBinderMetaVar prec | ETIdent -> - UnpBinderMetaVar (i,prec) + UnpBinderMetaVar prec | ETBinder isopen -> assert false @@ -453,10 +453,10 @@ let make_hunks etyps symbols from_level = (* We add NonTerminal for simulation but remove it afterwards *) else make true sl in let hunk = match typ with - | ETConstr _ -> UnpListMetaVar (i,prec,List.map snd sl') + | ETConstr _ -> UnpListMetaVar (prec,List.map snd sl') | ETBinder isopen -> check_open_binder isopen sl m; - UnpBinderListMetaVar (i,isopen,List.map snd sl') + UnpBinderListMetaVar (isopen,List.map snd sl') | _ -> assert false in (None, hunk) :: make_with_space b prods @@ -595,10 +595,10 @@ let hunks_of_format (from_level,(vars,typs)) symfmt = if not (List.is_empty sl) then error_format ?loc:(find_prod_list_loc loc_slfmt fmt) (); let symbs, l = aux (symbs,rfmt) in let hunk = match typ with - | ETConstr _ -> UnpListMetaVar (i,prec,slfmt) + | ETConstr _ -> UnpListMetaVar (prec,slfmt) | ETBinder isopen -> check_open_binder isopen sl m; - UnpBinderListMetaVar (i,isopen,slfmt) + UnpBinderListMetaVar (isopen,slfmt) | _ -> assert false in symbs, hunk :: l | symbs, (_,UnpBox (a,b)) :: fmt -> |