diff options
Diffstat (limited to 'parsing/egrammar.ml')
| -rw-r--r-- | parsing/egrammar.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index a477e3fd4b..1793be4134 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -111,24 +111,24 @@ let make_constr_prod_item univ assoc from forpat = function let eobj = symbol_of_production assoc from forpat nt in (eobj, ovar) -let extend_constr entry (n,assoc,pos,p4assoc,name) mkact (forpat,pt) = +let extend_constr entry (n,assoc,pos,p4assoc,name,reinit) mkact (forpat,pt) = let univ = get_univ "constr" in let pil = List.map (make_constr_prod_item univ assoc n forpat) pt in let (symbs,ntl) = List.split pil in - grammar_extend entry pos [(name, p4assoc, [symbs, mkact ntl])] + grammar_extend entry pos reinit [(name, p4assoc, [symbs, mkact ntl])] let extend_constr_notation (n,assoc,ntn,rule) = (* Add the notation in constr *) let mkact loc env = CNotation (loc,ntn,List.map snd env) in let (e,level,keepassoc) = get_constr_entry false (ETConstr (n,())) in - let pos,p4assoc,name = find_position false keepassoc assoc level in - extend_constr e (ETConstr(n,()),assoc,pos,p4assoc,name) + let pos,p4assoc,name,reinit = find_position false keepassoc assoc level in + extend_constr e (ETConstr(n,()),assoc,pos,p4assoc,name,reinit) (make_constr_action mkact) (false,rule); (* Add the notation in cases_pattern *) let mkact loc env = CPatNotation (loc,ntn,List.map snd env) in let (e,level,keepassoc) = get_constr_entry true (ETConstr (n,())) in - let pos,p4assoc,name = find_position true keepassoc assoc level in - extend_constr e (ETConstr (n,()),assoc,pos,p4assoc,name) + let pos,p4assoc,name,reinit = find_position true keepassoc assoc level in + extend_constr e (ETConstr (n,()),assoc,pos,p4assoc,name,reinit) (make_cases_pattern_action mkact) (true,rule) (**********************************************************************) @@ -266,7 +266,7 @@ let add_tactic_entry (key,lev,prods,tac) = (TacAtom(loc,TacAlias(loc,s,l,tac)):raw_tactic_expr) in make_rule univ (mkact key tac) mkprod prods in let _ = find_position true true None None (* to synchronise with remove *) in - grammar_extend entry pos [(None, None, List.rev [rules])] + grammar_extend entry pos None [(None, None, List.rev [rules])] (**********************************************************************) (** State of the grammar extensions *) |