diff options
| author | herbelin | 2006-01-11 09:47:32 +0000 |
|---|---|---|
| committer | herbelin | 2006-01-11 09:47:32 +0000 |
| commit | dcaefd4a668617504aaf335ed346598b03a80ba1 (patch) | |
| tree | 9b97ca322252777d101152452193d0a7c8537e2e /tactics/tacinterp.ml | |
| parent | 88d15de0cc467368dc71851e995d82093f9692ca (diff) | |
Restructuration et simplification des fonctions d'affichage, de détypage
et d'"externalisation"; standardisation du nom des fonctions d'affichage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 8f537a601f..8d4d37f426 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -114,8 +114,8 @@ let pr_value env = function | VVoid -> str "()" | VInteger n -> int n | VIntroPattern ipat -> pr_intro_pattern ipat - | VConstr c -> prterm_env env c - | VConstr_context c -> prterm_env env c + | VConstr c -> pr_lconstr_env env c + | VConstr_context c -> pr_lconstr_env env c | (VTactic _ | VRTactic _ | VFun _ | VRec _) -> str "<fun>" (* Transforms a named_context into a (string * constr) list *) @@ -1917,7 +1917,7 @@ let subst_global_reference subst = let ref',t' = subst_global subst ref in if not (eq_constr (constr_of_global ref') t') then ppnl (str "Warning: the reference " ++ pr_global ref ++ str " is not " ++ - str " expanded to \"" ++ prterm t' ++ str "\", but to " ++ + str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++ pr_global ref') ; ref' in |