- ported to typed explicit substitutions

[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 4b8099fed004c7e92ab152f190b5ca5599fde050..f5684a9510196194727e7a9e48bc9aaf2954146d 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
@@ -544,7 +544,7 @@ if List.mem uri params then prerr_endline "---- OK2" ;
           )
      | (k, e, ens, (C.Meta (n,l) as t), s) ->
         (try 
-          let (_, term) = CicUtil.lookup_subst n subst in
+          let (_, term,_) = CicUtil.lookup_subst n subst in
            reduce (k, e, ens,CicSubstitution.lift_meta l term,s)
         with  CicUtil.Subst_not_found _ ->
            let t' = unwind k e ens t in