From 63b530234e0b19323a50c52434a7439518565c81 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 24 May 2018 03:15:17 +0200 Subject: [notations] Split interpretation and parsing of notations Previously to this patch, `Notation_term` contained information about both parsing and notation interpretation. We split notation grammar to a file `parsing/notation_gram` as to make `interp/` not to depend on some parsing structures such as entries. --- interp/constrintern.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'interp/constrintern.ml') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 3a88284e4..45c0e9c42 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -820,11 +820,11 @@ let split_by_type ids subst = | NtnTypeConstr -> let terms,terms' = bind id scl terms terms' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') - | NtnTypeBinder NtnBinderParsedAsConstr (Extend.AsIdentOrPattern | Extend.AsStrictPattern) -> + | NtnTypeBinder NtnBinderParsedAsConstr (AsIdentOrPattern | AsStrictPattern) -> let a,terms = match terms with a::terms -> a,terms | _ -> assert false in let binders' = Id.Map.add id (coerce_to_cases_pattern_expr a,(false,scl)) binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') - | NtnTypeBinder NtnBinderParsedAsConstr Extend.AsIdent -> + | NtnTypeBinder NtnBinderParsedAsConstr AsIdent -> let a,terms = match terms with a::terms -> a,terms | _ -> assert false in let binders' = Id.Map.add id (cases_pattern_of_name (coerce_to_name a),(true,scl)) binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') -- cgit v1.2.3