From 24cbdd6b6b83b878797f067a4ae358b0fc4c4337 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 7 Dec 2008 18:57:15 +0000
Subject: [PATCH] Bug fixed: every time we form a Prod, we must typecheck it
 before trying unification.

---
 helm/software/components/ng_refiner/nCicRefiner.ml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index d812279b8..191bd708c 100644
--- 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: " ^
-- 
2.39.2