diff options
| author | msozeau | 2006-11-10 15:45:50 +0000 |
|---|---|---|
| committer | msozeau | 2006-11-10 15:45:50 +0000 |
| commit | ffa5a8d728ef0dcf32e878e27b40976ae51d0657 (patch) | |
| tree | d8fb2904e28073788af537874929ddb4c97a6fcc /contrib/subtac/eterm.ml | |
| parent | 30d3733a13f7c51ebe80548a9eb09aa9bf089e61 (diff) | |
Work on mutual defs, various bug fixes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9360 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/subtac/eterm.ml')
| -rw-r--r-- | contrib/subtac/eterm.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml index 790e61a0a8..8ec1736309 100644 --- a/contrib/subtac/eterm.ml +++ b/contrib/subtac/eterm.ml @@ -141,7 +141,8 @@ let eterm_obligations name nclen evm t tycon = let hyps = trunc_named_context nclen hyps in trace (str "Named context is: " ++ Printer.pr_named_context (Global.env ()) hyps); let evtyp, deps = etype_of_evar l ev hyps in - trace (str "Evar " ++ str (string_of_int n) ++ str "'s type is: " ++ Termops.print_constr_env (Global.env ()) evtyp); + trace (str "Evar " ++ str (string_of_int n) ++ str "'s type is: " ++ Termops.print_constr_env (Global.env ()) evtyp ++ + str " depends on evars : " ++ str (Subtac_utils.string_of_intset deps)); let y' = (id, ((n, nstr), hyps, evtyp, deps)) in y' :: l) evn [] |