diff options
| author | letouzey | 2012-10-16 16:24:23 +0000 |
|---|---|---|
| committer | letouzey | 2012-10-16 16:24:23 +0000 |
| commit | 15daaa856a6dd1f97845c4f24fe27eaf4cdbdda0 (patch) | |
| tree | 0b5a33550e30f286ef65e7c12ea452c2b86da409 /tactics/rewrite.ml4 | |
| 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 'tactics/rewrite.ml4')
| -rw-r--r-- | tactics/rewrite.ml4 | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index f2075d07d5..bd6786a67f 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1379,8 +1379,9 @@ let pr_glob_constr_with_bindings_sign _ _ _ (ge : glob_constr_with_bindings_sign let pr_glob_constr_with_bindings _ _ _ (ge : glob_constr_with_bindings) = Printer.pr_glob_constr (fst (fst ge)) let pr_constr_expr_with_bindings prc _ _ (ge : constr_expr_with_bindings) = prc (fst ge) let interp_glob_constr_with_bindings ist gl c = Tacmach.project gl , (ist, c) -let glob_glob_constr_with_bindings ist l = Tacinterp.intern_constr_with_bindings ist l -let subst_glob_constr_with_bindings s c = subst_glob_with_bindings s c +let glob_glob_constr_with_bindings ist l = Tacintern.intern_constr_with_bindings ist l +let subst_glob_constr_with_bindings s c = + Tacsubst.subst_glob_with_bindings s c ARGUMENT EXTEND glob_constr_with_bindings @@ -1465,7 +1466,7 @@ type glob_strategy = (glob_constr_and_expr, Tacexpr.raw_red_expr) strategy_ast let interp_strategy ist gl s = let sigma = project gl in sigma, strategy_of_ast s -let glob_strategy ist s = map_strategy (Tacinterp.intern_constr ist) (fun c -> c) s +let glob_strategy ist s = map_strategy (Tacintern.intern_constr ist) (fun c -> c) s let subst_strategy s str = str let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>" |