diff options
| author | Emilio Jesus Gallego Arias | 2018-07-30 00:03:37 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-07-30 00:03:37 +0200 |
| commit | dd84c113a154742dff86328ebc758097e9aac8eb (patch) | |
| tree | 67795fb720516f564d074d55d9e2aa90e3d4e7f2 /interp/notation_ops.ml | |
| parent | 231f679965745a4d7677166e8d5f62a38ebde4e7 (diff) | |
| parent | 569ad299a8092778611fcc8ae2842151c4b276db (diff) | |
Merge PR #8115: Support for custom entries in notations (take 2, feature part)
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 7cde563cd2..06943ce7b9 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1008,9 +1008,9 @@ let remove_sigma x (terms,termlists,binders,binderlists) = let remove_bindinglist_sigma x (terms,termlists,binders,binderlists) = (terms,termlists,binders,Id.List.remove_assoc x binderlists) -let add_ldots_var metas = (ldots_var,((None,[]),NtnTypeConstr))::metas +let add_ldots_var metas = (ldots_var,((Constrexpr.InConstrEntrySomeLevel,(None,[])),NtnTypeConstr))::metas -let add_meta_bindinglist x metas = (x,((None,[]),NtnTypeBinderList))::metas +let add_meta_bindinglist x metas = (x,((Constrexpr.InConstrEntrySomeLevel,(None,[])),NtnTypeBinderList))::metas (* This tells if letins in the middle of binders should be included in the sequence of binders *) @@ -1055,7 +1055,7 @@ let match_binderlist match_fun alp metas sigma rest x y iter termin revert = let alp,sigma = bind_bindinglist_env alp sigma x bl in match_fun alp metas sigma rest termin -let add_meta_term x metas = (x,((None,[]),NtnTypeConstr))::metas +let add_meta_term x metas = (x,((Constrexpr.InConstrEntrySomeLevel,(None,[])),NtnTypeConstr))::metas (* Should reuse the scope of the partner of x! *) let match_termlist match_fun alp metas sigma rest x y iter termin revert = let rec aux sigma acc rest = |