X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReductionMachine.ml;h=d0e103521b88fedf16615c79c05cb2b79c8c858a;hb=37f08b2aba9f17d9d609ca0f57d607f437a3d3fc;hp=c69ef5b7595422b4f7bd6bb2121847c2099c6618;hpb=a61f397a3ea3acaf95a04a2aafbf1d3f223a2755;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
index c69ef5b75..d0e103521 100644
--- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
@@ -66,7 +66,7 @@ let unwind' m k e t =
                               else S.lift m t'
                   | None -> C.Rel (n-k))
     | C.Var _ as t  -> t
-    | C.Meta _ as t -> t
+    | C.Meta (i,l) as t -> t
     | C.Sort _ as t -> t
     | C.Implicit as t -> t
     | C.Cast (te,ty) -> C.Cast (unwind_aux m te, unwind_aux m ty) (*CSC ??? *)
@@ -380,3 +380,7 @@ in
 
 
 
+
+
+
+