Bug fixed: every time we form a Prod, we must typecheck it before trying

[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 7ea11f3120035edaf8d4c63e43f7be8830c270fd..191bd708c3e6abbf3b843f89b3723df66a3a54c9 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -99,7 +99,6 @@ let rec typeof
   ?(localise=fun _ -> Stdpp.dummy_loc) 
   ~look_for_coercion metasenv subst context term expty 
 =
-        prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context term);
   let force_ty metasenv subst context orig t infty expty =
     (*D*)inside 'F'; try let rc = 
     match expty with
@@ -386,6 +385,10 @@ and eat_prods
               (("_",C.Decl ty_arg) :: context) `Type
           in
           let flex_prod = C.Prod ("_", ty_arg, meta) in
+          (* next line grants that ty_args is a type *)
+          let metasenv,subst, flex_prod, _ =
+           typeof ~look_for_coercion ~localise metasenv subst
+            context flex_prod None in
           pp (lazy ( "UNIFICATION in CTX:\n"^ 
             NCicPp.ppcontext ~metasenv ~subst context
             ^ "\nOF: " ^