New experimental commit: metavariables representation is changed again,

[helm.git] / helm / ocaml / cic_proof_checking / cicReductionMachine.ml

diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
index c69ef5b7595422b4f7bd6bb2121847c2099c6618..d0e103521b88fedf16615c79c05cb2b79c8c858a 100644 (file)
--- 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
 
 
 
+
+
+
+