diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 15 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 31 |
2 files changed, 28 insertions, 18 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 608747d0e..754ad8526 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -233,9 +233,9 @@ let declare_assumption is_coe (local,p,kind) (c,ctx) imps impl nl (_,ident) = ma in (gr,inst,Lib.is_modtype_strict ()) -let interp_assumption evdref env bl c = +let interp_assumption evdref env impls bl c = let c = prod_constr_expr c bl in - let ty, impls = interp_type_evars_impls env evdref c in + let ty, impls = interp_type_evars_impls env evdref ~impls c in let evd, nf = nf_evars_and_universes !evdref in let ctx = Evd.universe_context_set evd in ((nf ty, ctx), impls) @@ -259,12 +259,15 @@ let do_assumptions (_, poly, _ as kind) nl l = l [] else l in - let _,l = List.fold_map (fun env (is_coe,(idl,c)) -> - let (t,ctx),imps = interp_assumption evdref env [] c in + let _,l = List.fold_map (fun (env,ienv) (is_coe,(idl,c)) -> + let (t,ctx),imps = interp_assumption evdref env ienv [] c in let env = push_named_context (List.map (fun (_,id) -> (id,None,t)) idl) env in - (env,((is_coe,idl),t,(ctx,imps)))) - env l + let ienv = List.fold_right (fun (_,id) ienv -> + let impls = compute_internalization_data env Variable t imps in + Id.Map.add id impls ienv) idl ienv in + ((env,ienv),((is_coe,idl),t,(ctx,imps)))) + (env,empty_internalization_env) l in let evd = solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref) in let l = List.map (on_pi2 (nf_evar evd)) l in diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index b3de3a7c7..0b0fd4ef1 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -61,31 +61,34 @@ let rec make_tags = function | GramNonTerminal (loc, etyp, _, po) :: l -> etyp :: make_tags l | [] -> [] +let make_fresh_key = + let id = Summary.ref ~name:"Tactic Notation counter" 0 in + fun () -> KerName.make + (Safe_typing.current_modpath (Global.safe_env ())) + (Global.current_dirpath ()) + (incr id; Label.make ("_" ^ string_of_int !id)) + type tactic_grammar_obj = { + tacobj_key : KerName.t; tacobj_local : locality_flag; tacobj_tacgram : tactic_grammar; tacobj_tacpp : Pptactic.pp_tactic; tacobj_body : Tacexpr.glob_tactic_expr } -let key k tobj = - let mp,dp,_ = KerName.repr k in - KerName.make mp dp - (Label.make ("_" ^ string_of_int (Hashtbl.hash tobj.tacobj_tacgram))) - -let cache_tactic_notation ((_,k), tobj) = - let key = key k tobj in +let cache_tactic_notation (_, tobj) = + let key = tobj.tacobj_key in Tacenv.register_alias key tobj.tacobj_body; Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram; Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp -let open_tactic_notation i ((_,k), tobj) = - let key = key k tobj in +let open_tactic_notation i (_, tobj) = + let key = tobj.tacobj_key in if Int.equal i 1 && not tobj.tacobj_local then Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram -let load_tactic_notation i ((_,k), tobj) = - let key = key k tobj in +let load_tactic_notation i (_, tobj) = + let key = tobj.tacobj_key in (** Only add the printing and interpretation rules. *) Tacenv.register_alias key tobj.tacobj_body; Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp; @@ -93,7 +96,10 @@ let load_tactic_notation i ((_,k), tobj) = Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram let subst_tactic_notation (subst, tobj) = - { tobj with tacobj_body = Tacsubst.subst_tactic subst tobj.tacobj_body; } + { tobj with + tacobj_key = Mod_subst.subst_kn subst tobj.tacobj_key; + tacobj_body = Tacsubst.subst_tactic subst tobj.tacobj_body; + } let classify_tactic_notation tacobj = Substitute tacobj @@ -123,6 +129,7 @@ let add_tactic_notation (local,n,prods,e) = tacgram_prods = prods; } in let tacobj = { + tacobj_key = make_fresh_key (); tacobj_local = local; tacobj_tacgram = parule; tacobj_tacpp = pprule; |