diff options
| author | jforest | 2006-05-23 11:12:54 +0000 |
|---|---|---|
| committer | jforest | 2006-05-23 11:12:54 +0000 |
| commit | c8b444fa1b9e6a3ba02f895a68e2e88612a6c04f (patch) | |
| tree | 09383f4e8664b3312da6c4474456854dbb9da6af | |
| parent | b67b91c9547f13dec4aec8c8bd0b4383c814d077 (diff) | |
cleanning code
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8847 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/recdef/recdef.ml4 | 16 |
1 files changed, 0 insertions, 16 deletions
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index 0c9d731c19..21ee8cf6b3 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -359,22 +359,6 @@ let rec list_cond_rewrite k def pmax cond_eqs le_proofs = let (na,_,eq_t') = destProd eq_t in let _,_,eq_t'' = destProd eq_t' in let na',_,_ = destProd eq_t'' in - msgnl (str "eq_id := " ++ Ppconstr.pr_id eq); - let k_id = - match na with - | Name id -> - msgnl (str "k_id := "++ Ppconstr.pr_id id); - id - | _ -> anomaly "k_id" - in - let def_id = - match na' with - | Name id -> id - | _ -> anomaly "def_id" - in - msgnl (str "k_id := "++ Ppconstr.pr_id k_id); - msgnl (str "def_id := "++ Ppconstr.pr_id def_id); - msgnl (str "eq_t := "++ Printer.pr_lconstr_env (pf_env g) eq_t); tclTHENS (general_rewrite_bindings false (mkVar eq, |