diff options
author | 2005-01-31 14:34:14 +0000 | |
---|---|---|
committer | 2005-01-31 14:34:14 +0000 | |
commit | e669490d0d5e6ed4bb45c895194791f01d038637 (patch) | |
tree | 4eb40b447e6573dbaa1cf593a2cae6758850cb7c /contrib/funind/tacinvutils.ml | |
parent | d334716fb2d09dd3304f98ee0dbf39275eac010b (diff) | |
parent | 6497f27021fec4e01f2182014f2bb1989b4707f9 (diff) |
Merge commit 'upstream/8.0pl2'
Diffstat (limited to 'contrib/funind/tacinvutils.ml')
-rw-r--r-- | contrib/funind/tacinvutils.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml index 758071ba..6e086d95 100644 --- a/contrib/funind/tacinvutils.ml +++ b/contrib/funind/tacinvutils.ml @@ -20,7 +20,8 @@ open Reductionops (*s printing of constr -- debugging *) -let msg x = () ;; let prterm c = str "" (* comment this to see debug msgs *) +(* comment this line to see debug msgs *) +let msg x = () ;; let prterm c = str "" (* uncomment this to see debugging *) let prconstr c = msg (str" " ++ prterm c ++ str"\n") let prlistconstr lc = List.iter prconstr lc @@ -67,6 +68,10 @@ let rec mkevarmap_from_listex lex = match lex with | [] -> Evd.empty | ((ex,_),typ)::lex' -> +(* let _ = prstr "mkevarmap" in + let _ = prstr ("evar n. " ^ string_of_int ex ^ " ") in + let _ = prstr "OF TYPE: " in + let _ = prconstr typ in*) let info ={ evar_concl = typ; evar_hyps = empty_named_context; |