From 094b577f61f105f0a92f3f84d7e739884dd993a7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 19 Nov 2017 05:11:18 +0100 Subject: [parser] Remove unnecessary statically initialized hook. Addded by c6d9d4fb142ef42634be25b60c0995b541e86629 ["Adding ability to put any pattern in binders, prefixed by a quote."] its current placement as well as the hook don't make a lot of sense. In particular, they prevent parts of Coq working without linking the parser. To this purpose, we need to consolidate the `Constrexpr` utilities. While we are at it we do so and remove the `Topconstr` module which is fully redundant with `Constrexpr_ops`. --- printing/ppconstr.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'printing') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 0f6452de6..bce5710d6 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -396,7 +396,7 @@ let tag_var = tag Tag.variable extract_prod_binders c | { loc; v = CProdN ([[_,Name id],bk,t], { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([_,[p]],b))])} ) } - when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) -> + when Id.equal id id' && not (Id.Set.mem id (free_vars_of_constr_expr b)) -> let bl,c = extract_prod_binders b in CLocalPattern (loc, (p,None)) :: bl, c | { loc; v = CProdN ((nal,bk,t)::bl,c) } -> @@ -412,7 +412,7 @@ let tag_var = tag Tag.variable extract_lam_binders c | CLambdaN ([[_,Name id],bk,t], { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([_,[p]],b))])} ) - when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) -> + when Id.equal id id' && not (Id.Set.mem id (free_vars_of_constr_expr b)) -> let bl,c = extract_lam_binders b in CLocalPattern (ce.loc,(p,None)) :: bl, c | CLambdaN ((nal,bk,t)::bl,c) -> @@ -430,7 +430,7 @@ let tag_var = tag Tag.variable let rename na na' t c = match (na,na') with | (_,Name id), (_,Name id') -> - (na',t,Topconstr.replace_vars_constr_expr (Id.Map.singleton id id') c) + (na',t,replace_vars_constr_expr (Id.Map.singleton id id') c) | (_,Name id), (_,Anonymous) -> (na,t,c) | _ -> (na',t,c) -- cgit v1.2.3