From 6b9a9124d3bd24fe9305df613547139f6f609c60 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 10 Aug 2017 16:15:57 +0200 Subject: Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr. The motivations are: - To reflect the concrete syntax more closely. - To factorize the different places where "contexts" are internalized: before this patch, there is a different treatment of `Definition f '(x,y) := x+y` and `Definition f := fun '(x,y) => x+y`, and a hack to interpret `Definition f `pat := c : t`. With the patch, the fix to avoid seeing a variable named `pat` works for both `fun 'x => ...` and `Definition f 'x := ...`. The drawbacks are: - Counterpart to reflecting the concrete syntax more closerly, there are more redundancies in the syntax. For instance, the case `CLetIn (na,b,t,c)` can appears also in the form `CProdN (CLocalDef (na,b,t)::rest,d)` and `CLambdaN (CLocalDef (na,b,t)::rest,d)`. - Changes in the API, hence adaptation of plugins referring to `constr_expr` needed. --- plugins/funind/glob_term_to_relation.ml | 8 ++++---- plugins/funind/indfun.ml | 34 +++++++++++++++++---------------- plugins/ltac/g_tactic.ml4 | 6 ++++-- plugins/ltac/pptactic.ml | 7 ++++--- plugins/ssr/ssrcommon.ml | 6 +++--- plugins/ssr/ssrparser.ml4 | 22 ++++++++++----------- plugins/ssrmatching/ssrmatching.ml4 | 2 +- 7 files changed, 45 insertions(+), 40 deletions(-) (limited to 'plugins') diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index f7639d22d6..693ab464d7 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1295,8 +1295,8 @@ let rec rebuild_return_type rt = CAst.make ?loc @@ Constrexpr.CProdN(n,rebuild_return_type t') | Constrexpr.CLetIn(na,v,t,t') -> CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t') - | _ -> CAst.make ?loc @@ Constrexpr.CProdN([[Loc.tag Anonymous], - Constrexpr.Default Decl_kinds.Explicit, rt], + | _ -> CAst.make ?loc @@ Constrexpr.CProdN([Constrexpr.CLocalAssum ([Loc.tag Anonymous], + Constrexpr.Default Decl_kinds.Explicit, rt)], CAst.make @@ Constrexpr.CSort(GType [])) let do_build_inductive @@ -1356,7 +1356,7 @@ let do_build_inductive acc) | None -> CAst.make @@ Constrexpr.CProdN - ([[(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], + ([Constrexpr.CLocalAssum([(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)], acc ) ) @@ -1423,7 +1423,7 @@ let do_build_inductive acc) | None -> CAst.make @@ Constrexpr.CProdN - ([[(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], + ([Constrexpr.CLocalAssum([(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)], acc ) ) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 58154d3106..96e4a94d3e 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -591,11 +591,11 @@ and rebuild_nal aux bk bl' nal typ = match nal,typ with | _,{ CAst.v = CProdN([],typ) } -> rebuild_nal aux bk bl' nal typ | [], _ -> rebuild_bl aux bl' typ - | na::nal,{ CAst.v = CProdN((na'::nal',bk',nal't)::rest,typ') } -> + | na::nal,{ CAst.v = CProdN(CLocalAssum(na'::nal',bk',nal't)::rest,typ') } -> if Name.equal (snd na) (snd na') || Name.is_anonymous (snd na') then let assum = CLocalAssum([na],bk,nal't) in - let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in + let new_rest = if nal' = [] then rest else (CLocalAssum(nal',bk',nal't)::rest) in rebuild_nal (assum::aux) bk @@ -604,7 +604,7 @@ and rebuild_nal aux bk bl' nal typ = (CAst.make @@ CProdN(new_rest,typ')) else let assum = CLocalAssum([na'],bk,nal't) in - let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in + let new_rest = if nal' = [] then rest else (CLocalAssum(nal',bk',nal't)::rest) in rebuild_nal (assum::aux) bk @@ -731,10 +731,14 @@ let rec add_args id new_args = CAst.map (function end | CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo.") | CProdN(nal,b1) -> - CProdN(List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, + CProdN(List.map (function CLocalAssum (nal,k,b2) -> CLocalAssum (nal,k,add_args id new_args b2) + | CLocalDef (na,b1,t) -> CLocalDef (na,add_args id new_args b1,Option.map (add_args id new_args) t) + | CLocalPattern _ -> user_err (Pp.str "pattern with quote not allowed here.")) nal, add_args id new_args b1) | CLambdaN(nal,b1) -> - CLambdaN(List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, + CLambdaN(List.map (function CLocalAssum (nal,k,b2) -> CLocalAssum (nal,k,add_args id new_args b2) + | CLocalDef (na,b1,t) -> CLocalDef (na,add_args id new_args b1,Option.map (add_args id new_args) t) + | CLocalPattern _ -> user_err (Pp.str "pattern with quote not allowed here.")) nal, add_args id new_args b1) | CLetIn(na,b1,t,b2) -> CLetIn(na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2) @@ -793,7 +797,7 @@ let rec chop_n_arrow n t = then t (* If we have already removed all the arrows then return the type *) else (* If not we check the form of [t] *) match t.CAst.v with - | Constrexpr.CProdN(nal_ta',t') -> (* If we have a forall, to result are possible : + | Constrexpr.CProdN(nal_ta',t') -> (* If we have a forall, two results are possible : either we need to discard more than the number of arrows contained in this product declaration then we just recall [chop_n_arrow] on the remaining number of arrow to chop and [t'] we discard it and @@ -805,7 +809,7 @@ let rec chop_n_arrow n t = let new_n = let rec aux (n:int) = function [] -> n - | (nal,k,t'')::nal_ta' -> + | CLocalAssum(nal,k,t'')::nal_ta' -> let nal_l = List.length nal in if n >= nal_l then @@ -813,9 +817,10 @@ let rec chop_n_arrow n t = else let new_t' = CAst.make @@ Constrexpr.CProdN( - ((snd (List.chop n nal)),k,t'')::nal_ta',t') + CLocalAssum((snd (List.chop n nal)),k,t'')::nal_ta',t') in raise (Stop new_t') + | _ -> anomaly (Pp.str "Not enough products.") in aux n nal_ta' in @@ -828,16 +833,13 @@ let rec chop_n_arrow n t = let rec get_args b t : Constrexpr.local_binder_expr list * Constrexpr.constr_expr * Constrexpr.constr_expr = match b.CAst.v with - | Constrexpr.CLambdaN ((nal_ta), b') -> + | Constrexpr.CLambdaN (CLocalAssum(nal,k,ta) as d::rest, b') -> begin - let n = - (List.fold_left (fun n (nal,_,_) -> - n+List.length nal) 0 nal_ta ) - in - let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in - (List.map (fun (nal,k,ta) -> - (Constrexpr.CLocalAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t'' + let n = List.length nal in + let nal_tas,b'',t'' = get_args (CAst.make ?loc:b.CAst.loc @@ Constrexpr.CLambdaN (rest,b')) (chop_n_arrow n t) in + d :: nal_tas, b'',t'' end + | Constrexpr.CLambdaN ([], b) -> [],b,t | _ -> [],b,t diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index d792d4ff7d..e68140828a 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -115,10 +115,11 @@ let mk_fix_tac (loc,id,bl,ann,ty) = match bl,ann with [([_],_,_)], None -> 1 | _, Some x -> - let ids = List.map snd (List.flatten (List.map pi1 bl)) in + let ids = List.map snd (List.flatten (List.map (fun (nal,_,_) -> nal) bl)) in (try List.index Names.Name.equal (snd x) ids with Not_found -> user_err Pp.(str "No such fix variable.")) | _ -> user_err Pp.(str "Cannot guess decreasing argument of fix.") in + let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,bk,t)) bl in (id,n, CAst.make ~loc @@ CProdN(bl,ty)) let mk_cofix_tac (loc,id,bl,ann,ty) = @@ -126,6 +127,7 @@ let mk_cofix_tac (loc,id,bl,ann,ty) = user_err ~loc:aloc ~hdr:"Constr:mk_cofix_tac" (Pp.str"Annotation forbidden in cofix expression.")) ann in + let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,bk,t)) bl in (id,CAst.make ~loc @@ CProdN(bl,ty)) (* Functions overloaded by quotifier *) @@ -160,7 +162,7 @@ let mkTacCase with_evar = function let rec mkCLambdaN_simple_loc ?loc bll c = match bll with | ((loc1,_)::_ as idl,bk,t) :: bll -> - CAst.make ?loc @@ CLambdaN ([idl,bk,t],mkCLambdaN_simple_loc ?loc:(Loc.merge_opt loc1 loc) bll c) + CAst.make ?loc @@ CLambdaN ([CLocalAssum (idl,bk,t)],mkCLambdaN_simple_loc ?loc:(Loc.merge_opt loc1 loc) bll c) | ([],_,_) :: bll -> mkCLambdaN_simple_loc ?loc bll c | [] -> c diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index e5ff473568..4f430b79e4 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -353,9 +353,10 @@ let string_of_genarg_arg (ArgumentType arg) = let rec strip_ty acc n ty = match ty.CAst.v with Constrexpr.CProdN(bll,a) -> - let nb = - List.fold_left (fun i (nal,_,_) -> i + List.length nal) 0 bll in - let bll = List.map (fun (x, _, y) -> x, y) bll in + let bll = List.map (function + | CLocalAssum (nal,_,t) -> nal,t + | _ -> user_err Pp.(str "Cannot translate fix tactic: not only products")) bll in + let nb = List.fold_left (fun i (nal,t) -> i + List.length nal) 0 bll in if nb >= n then (List.rev (bll@acc)), a else strip_ty (bll@acc) (n-nb) a | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 9822da1c7e..499154d503 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -835,9 +835,9 @@ let rec mkCHoles ?loc n = if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) :: mkCHoles ?loc (n - 1) let mkCHole loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None) let mkCLambda ?loc name ty t = CAst.make ?loc @@ - CLambdaN ([[loc, name], Default Explicit, ty], t) + CLambdaN ([CLocalAssum([loc, name], Default Explicit, ty)], t) let mkCArrow ?loc ty t = CAst.make ?loc @@ - CProdN ([[Loc.tag Anonymous], Default Explicit, ty], t) + CProdN ([CLocalAssum([Loc.tag Anonymous], Default Explicit, ty)], t) let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, CastConv ty) let rec isCHoles = function { CAst.v = CHole _ } :: cl -> isCHoles cl | cl -> cl = [] @@ -855,7 +855,7 @@ let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty = | _, (_, Some ty) -> let rec force_type ty = CAst.(map (function | CProdN (abs, t) -> - n_binders := !n_binders + List.length (List.flatten (List.map pi1 abs)); + n_binders := !n_binders + List.length (List.flatten (List.map (function CLocalAssum (nal,_,_) -> nal | CLocalDef (na,_,_) -> [na] | CLocalPattern (_,_) -> (* We count a 'pat for 1; TO BE CHECKED *) [Loc.tag Name.Anonymous]) abs)); CProdN (abs, force_type t) | CLetIn (n, v, oty, t) -> incr n_binders; CLetIn (n, v, oty, force_type t) | _ -> (mkCCast ty (mkCType None)).v)) ty in diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 46403aef3c..211cad3f58 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -1023,10 +1023,10 @@ let rec format_local_binders h0 bl0 = match h0, bl0 with | _ -> [] let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with - | BFvar :: h, { v = CLambdaN ([[_, x], _, _], c) } -> + | BFvar :: h, { v = CLambdaN ([CLocalAssum([_, x], _, _)], c) } -> let bs, c' = format_constr_expr h c in Bvar x :: bs, c' - | BFdecl _:: h, { v = CLambdaN ([lxs, _, t], c) } -> + | BFdecl _:: h, { v = CLambdaN ([CLocalAssum(lxs, _, t)], c) } -> let bs, c' = format_constr_expr h c in Bdecl (List.map snd lxs, t) :: bs, c' | BFdef :: h, { v = CLetIn((_, x), v, oty, c) } -> @@ -1165,20 +1165,20 @@ ARGUMENT EXTEND ssrbinder TYPED AS ssrfwdfmt * constr PRINTED BY pr_ssrbinder | [ ssrbvar(bv) ] -> [ let xloc, _ as x = bvar_lname bv in (FwdPose, [BFvar]), - CAst.make ~loc @@ CLambdaN ([[x],Default Explicit,mkCHole xloc],mkCHole (Some loc)) ] + CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) ] | [ "(" ssrbvar(bv) ")" ] -> [ let xloc, _ as x = bvar_lname bv in (FwdPose, [BFvar]), - CAst.make ~loc @@ CLambdaN ([[x],Default Explicit,mkCHole xloc],mkCHole (Some loc)) ] + CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) ] | [ "(" ssrbvar(bv) ":" lconstr(t) ")" ] -> [ let x = bvar_lname bv in (FwdPose, [BFdecl 1]), - CAst.make ~loc @@ CLambdaN ([[x], Default Explicit, t], mkCHole (Some loc)) ] + CAst.make ~loc @@ CLambdaN ([CLocalAssum([x], Default Explicit, t)], mkCHole (Some loc)) ] | [ "(" ssrbvar(bv) ne_ssrbvar_list(bvs) ":" lconstr(t) ")" ] -> [ let xs = List.map bvar_lname (bv :: bvs) in let n = List.length xs in (FwdPose, [BFdecl n]), - CAst.make ~loc @@ CLambdaN ([xs, Default Explicit, t], mkCHole (Some loc)) ] + CAst.make ~loc @@ CLambdaN ([CLocalAssum (xs, Default Explicit, t)], mkCHole (Some loc)) ] | [ "(" ssrbvar(id) ":" lconstr(t) ":=" lconstr(v) ")" ] -> [ (FwdPose,[BFdef]), CAst.make ~loc @@ CLetIn (bvar_lname id, v, Some t, mkCHole (Some loc)) ] | [ "(" ssrbvar(id) ":=" lconstr(v) ")" ] -> @@ -1191,7 +1191,7 @@ GEXTEND Gram [ ["of" | "&"]; c = operconstr LEVEL "99" -> let loc = !@loc in (FwdPose, [BFvar]), - CAst.make ~loc @@ CLambdaN ([[Loc.tag ~loc Anonymous],Default Explicit,c],mkCHole (Some loc)) ] + CAst.make ~loc @@ CLambdaN ([CLocalAssum ([Loc.tag ~loc Anonymous],Default Explicit,c)],mkCHole (Some loc)) ] ]; END @@ -1217,7 +1217,7 @@ let push_binders c2 bs = | ct -> loop false ct bs let rec fix_binders = let open CAst in function - | (_, { v = CLambdaN ([xs, _, t], _) } ) :: bs -> + | (_, { v = CLambdaN ([CLocalAssum(xs, _, t)], _) } ) :: bs -> CLocalAssum (xs, Default Explicit, t) :: fix_binders bs | (_, { v = CLetIn (x, v, oty, _) } ) :: bs -> CLocalDef (x, v, oty) :: fix_binders bs @@ -1325,13 +1325,13 @@ let intro_id_to_binder = List.map (function | IPatId id -> let xloc, _ as x = bvar_lname (mkCVar id) in (FwdPose, [BFvar]), - CAst.make @@ CLambdaN ([[x], Default Explicit, mkCHole xloc], + CAst.make @@ CLambdaN ([CLocalAssum([x], Default Explicit, mkCHole xloc)], mkCHole None) | _ -> anomaly "non-id accepted as binder") let binder_to_intro_id = CAst.(List.map (function - | (FwdPose, [BFvar]), { v = CLambdaN ([ids,_,_],_) } - | (FwdPose, [BFdecl _]), { v = CLambdaN ([ids,_,_],_) } -> + | (FwdPose, [BFvar]), { v = CLambdaN ([CLocalAssum(ids,_,_)],_) } + | (FwdPose, [BFdecl _]), { v = CLambdaN ([CLocalAssum(ids,_,_)],_) } -> List.map (function (_, Name id) -> IPatId id | _ -> IPatAnon One) ids | (FwdPose, [BFdef]), { v = CLetIn ((_,Name id),_,_,_) } -> [IPatId id] | (FwdPose, [BFdef]), { v = CLetIn ((_,Anonymous),_,_,_) } -> [IPatAnon One] diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 7d0584a00d..17409595aa 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -137,7 +137,7 @@ let destGLambda c = match DAst.get c with GLambda (Name id, _, _, c) -> (id, c) let isGHole c = match DAst.get c with GHole _ -> true | _ -> false let mkCHole ~loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None) let mkCLambda ?loc name ty t = CAst.make ?loc @@ - CLambdaN ([[Loc.tag ?loc name], Default Explicit, ty], t) + CLambdaN ([CLocalAssum([Loc.tag ?loc name], Default Explicit, ty)], t) let mkCLetIn ?loc name bo t = CAst.make ?loc @@ CLetIn ((Loc.tag ?loc name), bo, None, t) let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, dC ty) -- cgit v1.2.3 From 398358618bb3eabfe822b79c669703c1c33b67e6 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 15 Aug 2017 18:32:02 +0200 Subject: Adding patterns in the category of binders for notations. For instance, the following is now possible: Check {(x,y)|x+y=0}. Some questions remains. Maybe, by consistency, the notation should be "{'(x,y)|x+y=0}"... --- plugins/ssr/ssrvernac.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins') diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index d74ad06b34..db18fab24e 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -298,7 +298,7 @@ let interp_search_notation ?loc tag okey = let rec sub () = function | NVar x when List.mem_assoc x nvars -> DAst.make ?loc @@ GPatVar (FirstOrderPatVar x) | c -> - glob_constr_of_notation_constr_with_binders ?loc (fun _ x -> (), x) sub () c in + glob_constr_of_notation_constr_with_binders ?loc (fun _ x -> (), None, x) sub () c in let _, npat = Patternops.pattern_of_glob_constr (sub () body) in Search.GlobSearchSubPattern npat -- cgit v1.2.3 From edd0d22429354a5f2c703a8c7bd1f775e2f97d9e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Aug 2017 09:15:40 +0200 Subject: Adding support for parsing subterms of a notation as "pattern". This allows in particular to define notations with 'pat style binders. E.g.: A non-trivial change in this commit is storing binders and patterns separately from terms. This is not strictly necessary but has some advantages. However, it is relatively common to have binders also used as terms, or binders parsed as terms. Thus, it is already relatively common to embed binders into terms (see e.g. notation for ETA in output test Notations3.v) or to coerce terms to idents (see e.g. the notation for {x|P} where x is parsed as a constr). So, it is as simple to always store idents (and eventually patterns) as terms. --- plugins/ssr/ssrvernac.ml4 | 2 +- plugins/ssrmatching/ssrmatching.ml4 | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) (limited to 'plugins') diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index db18fab24e..25d1472f19 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -74,7 +74,7 @@ let frozen_lexer = CLexer.get_keyword_state () ;; let no_ct = None, None and no_rt = None in let aliasvar = function - | [[{ CAst.v = CPatAlias (_, id); loc }]] -> Some (loc,Name id) + | [[{ CAst.v = CPatAlias (_, na); loc }]] -> Some na | _ -> None in let mk_cnotype mp = aliasvar mp, None in let mk_ctype mp t = aliasvar mp, Some t in diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 17409595aa..71e8b4ac46 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -916,7 +916,7 @@ let glob_cpattern gs p = | k, (v, Some t) as orig -> if k = 'x' then glob_ssrterm gs ('(', (v, Some t)) else match t.CAst.v with - | CNotation("( _ in _ )", ([t1; t2], [], [])) -> + | CNotation("( _ in _ )", ([t1; t2], [], [], [])) -> (try match glob t1, glob t2 with | (r1, None), (r2, None) -> encode k "In" [r1;r2] | (r1, Some _), (r2, Some _) when isCVar t1 -> @@ -924,11 +924,11 @@ let glob_cpattern gs p = | (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2] | _ -> CErrors.anomaly (str"where are we?.") with _ when isCVar t1 -> encode k "In" [bind_in t1 t2]) - | CNotation("( _ in _ in _ )", ([t1; t2; t3], [], [])) -> + | CNotation("( _ in _ in _ )", ([t1; t2; t3], [], [], [])) -> check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3] - | CNotation("( _ as _ )", ([t1; t2], [], [])) -> + | CNotation("( _ as _ )", ([t1; t2], [], [], [])) -> encode k "As" [fst (glob t1); fst (glob t2)] - | CNotation("( _ as _ in _ )", ([t1; t2; t3], [], [])) -> + | CNotation("( _ as _ in _ )", ([t1; t2; t3], [], [], [])) -> check_var t2; encode k "As" [fst (glob t1); bind_in t2 t3] | _ -> glob_ssrterm gs orig ;; -- cgit v1.2.3 From 69822345c198aa6bf51354f6b84c7fd5d401bc9c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 23 Aug 2017 20:32:15 +0200 Subject: Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq. Renaming it register_grammars_by_name. --- plugins/ltac/tacentries.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'plugins') diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index ee84be5414..8112cc4008 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -545,11 +545,10 @@ let print_located_tactic qid = (** Grammar *) let () = - let open Metasyntax in let entries = [ AnyEntry Pltac.tactic_expr; AnyEntry Pltac.binder_tactic; AnyEntry Pltac.simple_tactic; AnyEntry Pltac.tactic_arg; ] in - register_grammar "tactic" entries + register_grammars_by_name "tactic" entries -- cgit v1.2.3