From 7da6488b45e5dfc1b675552a7f19c58a6abbff2b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 7 Jun 2011 12:13:27 +0000 Subject: [PATCH] This can happen: when you use nodelta. --- matita/components/ng_tactics/nCicTacReduction.ml | 1 - 1 file changed, 1 deletion(-) 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 -- 2.39.2