From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 7 Jun 2011 12:13:27 +0000 (+0000)
Subject: This can happen: when you use nodelta.
X-Git-Tag: make_still_working~2457
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7da6488b45e5dfc1b675552a7f19c58a6abbff2b;p=helm.git

This can happen: when you use nodelta.
---

diff --git a/matita/components/ng_tactics/nCicTacReduction.ml b/matita/components/ng_tactics/nCicTacReduction.ml
index c1eba801f..96a795c34 100644
--- a/matita/components/ng_tactics/nCicTacReduction.ml
+++ b/matita/components/ng_tactics/nCicTacReduction.ml
@@ -15,7 +15,6 @@ let rec normalize status ?(delta=0) ~subst ctx t =
  normalize_machine status ~delta ~subst ctx
   (fst (NCicReduction.reduce_machine status ~delta ~subst ctx (0,[],t,[])))
 and normalize_machine status ?(delta=0) ~subst ctx (k,e,t,s) =
- assert (delta=0);
  let t = 
    if k = 0 then t
    else