diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-16 16:24:23 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-16 16:24:23 +0000 |
| commit | 15daaa856a6dd1f97845c4f24fe27eaf4cdbdda0 (patch) | |
| tree | 0b5a33550e30f286ef65e7c12ea452c2b86da409 /toplevel | |
| parent | 3b5927180128a4e8f10f7437641ff3af220194b3 (diff) | |
Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15896 85f007b7-540e-0410-9357-904b9bb8a0f7
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 e7c19fbb2..ed6b45228 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 016f0c60a..fa0068998 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)) |