X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReduction.ml;h=aaca61942aa323467bfb0d29a4914f3405681005;hb=c27b932e5adcf89dc9de0e28f65e3370fe3e6b05;hp=8b9a0d22e35bc4d2b7d36d70cb4a6291a2178604;hpb=219fb7c39077e9c82b3657ab067c176bb5b222ef;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml
index 8b9a0d22e..aaca61942 100644
--- a/helm/ocaml/cic_proof_checking/cicReduction.ml
+++ b/helm/ocaml/cic_proof_checking/cicReduction.ml
@@ -1063,8 +1063,8 @@ let rec normalize ?(delta=true) ?(subst=[]) ctx term =
       let s' = aux ctx s in
       C.Lambda (n, s', aux ((decl n s')::ctx) t)
   | C.LetIn (n,s,t) ->
-      let s' = aux ctx s in
-      C.LetIn (n, s, aux ((def n s')::ctx) t)
+      (* the term is already in weak head normal form *)
+      assert false
   | C.Appl (h::l) -> C.Appl (h::(List.map (aux ctx) l))
   | C.Appl [] -> assert false
   | C.Const (uri,exp_named_subst) ->
@@ -1076,6 +1076,7 @@ let rec normalize ?(delta=true) ?(subst=[]) ctx term =
         List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
   | C.MutCase (sp,i,outt,t,pl) ->
       C.MutCase (sp,i, aux ctx outt, aux ctx t, List.map (aux ctx) pl)
+(*CSC: to be completed, I suppose *)
   | C.Fix _ -> t 
   | C.CoFix _ -> t