X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReduction.ml;h=14b858491d8c55c8e4c9010ecb5781836e796845;hb=ed9af5a10b66343f817a1f9eac3add29e4b2baae;hp=63a8f550323a8ac9ad9fd8fd90b609158ef230f4;hpb=d3af4c289c9870337a141a0ffa98f9e01439d806;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml
index 63a8f5503..14b858491 100644
--- a/helm/ocaml/cic_proof_checking/cicReduction.ml
+++ b/helm/ocaml/cic_proof_checking/cicReduction.ml
@@ -1086,3 +1086,19 @@ let normalize ?delta ?subst ctx term =
   t
   
   
+(* performs an head beta/cast reduction *)
+let rec head_beta_reduce =
+ function
+    (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
+      let he'' = CicSubstitution.subst he' t in
+       if tl' = [] then
+        he''
+       else
+        let he''' =
+         match he'' with
+            Cic.Appl l -> Cic.Appl (l@tl')
+          | _ -> Cic.Appl (he''::tl')
+        in
+         head_beta_reduce he'''
+  | Cic.Cast (te,_) -> head_beta_reduce te
+  | t -> t