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

unification.

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index d812279b8c68eed15d00c337da7f0dd821dccd0b..191bd708c3e6abbf3b843f89b3723df66a3a54c9 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -385,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: " ^