diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/metasyntax.ml | 4 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 6 |
2 files changed, 5 insertions, 5 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index e7c19fbb21..ed6b452282 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -73,7 +73,7 @@ let cache_tactic_notation (_, tobj) = let subst_tactic_parule subst tg = let dir, tac = tg.tacgram_tactic in - { tg with tacgram_tactic = (dir, Tacinterp.subst_tactic subst tac); } + { tg with tacgram_tactic = (dir, Tacsubst.subst_tactic subst tac); } let subst_tactic_notation (subst, tobj) = { tobj with @@ -112,7 +112,7 @@ let add_tactic_notation (local,n,prods,e) = pptac_prods = (n, List.map make_terminal_status prods); } in let ids = List.fold_left cons_production_parameter [] prods in - let tac = Tacinterp.glob_tactic_env ids (Global.env()) e in + let tac = Tacintern.glob_tactic_env ids (Global.env()) e in let parule = { tacgram_key = key; tacgram_level = n; diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 016f0c60af..fa00689982 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -876,7 +876,7 @@ let vernac_restore_state file = (* Commands *) let vernac_declare_tactic_definition (local,x,def) = - Tacinterp.add_tacdef local x def + Tacintern.add_tacdef local x def let vernac_create_hintdb local id b = Auto.create_hint_db local id full_transparent_state b @@ -1317,7 +1317,7 @@ let vernac_check_may_eval redexp glopt rc = | None -> msg_notice (print_judgment env j) | Some r -> - Tacinterp.dump_glob_red_expr r; + Tacintern.dump_glob_red_expr r; let (sigma',r_interp) = interp_redexp env sigma' r in let redfun = fst (reduction_of_red_expr r_interp) in msg_notice (print_eval redfun env sigma' rc j) @@ -1352,7 +1352,7 @@ let vernac_print = function | PrintClasses -> msg_notice (Prettyp.print_classes()) | PrintTypeClasses -> msg_notice (Prettyp.print_typeclasses()) | PrintInstances c -> msg_notice (Prettyp.print_instances (smart_global c)) - | PrintLtac qid -> msg_notice (Tacinterp.print_ltac (snd (qualid_of_reference qid))) + | PrintLtac qid -> msg_notice (Tacintern.print_ltac (snd (qualid_of_reference qid))) | PrintCoercions -> msg_notice (Prettyp.print_coercions()) | PrintCoercionPaths (cls,clt) -> msg_notice (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt)) |