From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 7 Dec 2008 18:57:15 +0000 (+0000)
Subject: Bug fixed: every time we form a Prod, we must typecheck it before trying
X-Git-Tag: make_still_working~4439
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=24cbdd6b6b83b878797f067a4ae358b0fc4c4337;p=helm.git

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 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: " ^