a few missing ~subst added to whd

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

diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml
index 2fc29d5978193fa19f0d3b18e3a1f4d302ae3981..b8f31c805e18c414c1b1f85c5bdde2043ee86b70 100644 (file)
--- a/helm/software/components/ng_refiner/nCicCoercion.ml
+++ b/helm/software/components/ng_refiner/nCicCoercion.ml
@@ -40,7 +40,8 @@ let db () =
             let arity = match tgt with | CoercDb.Fun i -> i | _ -> 0 in
             let src, tgt = 
               let cty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] c in
-              match NCicMetaSubst.saturate ~delta:max_int [] [] cty (arity+1) 
+              match 
+               NCicMetaSubst.saturate ~delta:max_int [] [] [] cty (arity+1) 
               with
               | NCic.Prod (_, src, tgt),_,_ -> 
                 src, NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) tgt 
@@ -58,8 +59,7 @@ let db () =
     (DB.empty,DB.empty) (CoercDb.to_list ())
 ;;
 
-(* XXX saturate takes no subst!!!! *)
-let look_for_coercion (db_src,db_tgt) metasenv _subst context infty expty =
+let look_for_coercion (db_src,db_tgt) metasenv subst context infty expty =
   let set_src = DB.retrieve_unifiables db_src infty in
   let set_tgt = DB.retrieve_unifiables db_tgt expty in
   let candidates = CoercionSet.inter set_src set_tgt in
@@ -68,11 +68,11 @@ let look_for_coercion (db_src,db_tgt) metasenv _subst context infty expty =
     (fun (t,arity,arg) ->
         let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t in
         let ty, metasenv, args = 
-          NCicMetaSubst.saturate ~delta:max_int metasenv context ty arity
+          NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty arity
         in
         prerr_endline (
           NCicPp.ppterm ~metasenv ~subst:[] ~context:[] ty ^ " --- " ^ 
-          NCicPp.ppterm ~metasenv ~subst:_subst ~context
+          NCicPp.ppterm ~metasenv ~subst ~context
           (NCicUntrusted.mk_appl t args) ^ " --- " ^ 
             string_of_int (List.length args) ^ " == " ^ string_of_int arg);
         metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)