a few missing ~subst added to whd

[helm.git] / helm / software / components / ng_refiner / nCicRefiner.ml

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index e9d0e97fd8e9f3ede237fdb4185a2c3bd4b18aba..7ea11f3120035edaf8d4c63e43f7be8830c270fd 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -225,7 +225,7 @@ let rec typeof
       let _, _, arity, cl = List.nth itl tyno in
       let constructorsno = List.length cl in
       let _, metasenv, args = 
-        NCicMetaSubst.saturate metasenv context arity 0 in
+        NCicMetaSubst.saturate metasenv subst context arity 0 in
       let ind = if args = [] then C.Const r else C.Appl (C.Const r::args) in
       let metasenv, subst, term, _ = 
         typeof_aux metasenv subst context (Some ind) term in