From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 29 Jun 2012 14:25:43 +0000 (+0000)
Subject: Bug fixed: arguments of a match are (no longer...) in whd; so a function
X-Git-Tag: make_still_working~1626
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6120c5ba6c24eeeb2f932ba7e247a751c4216134;p=helm.git

Bug fixed: arguments of a match are (no longer...) in whd; so a function
that expects a term in whd was calling herself recursively on a term not
in whd.
---

diff --git a/matita/components/ng_refiner/nCicUnification.ml b/matita/components/ng_refiner/nCicUnification.ml
index b4bc32fe6..6dfa7afee 100644
--- a/matita/components/ng_refiner/nCicUnification.ml
+++ b/matita/components/ng_refiner/nCicUnification.ml
@@ -141,7 +141,9 @@ let rec could_reduce status ~subst context =
      when List.length args > recno ->
       let t = NCicReduction.whd status ~subst context (List.nth args recno) in
         could_reduce status subst context t
-  | C.Match (_,_,arg,_) -> could_reduce status ~subst context arg
+  | C.Match (_,_,he,_) ->
+     let he = NCicReduction.whd status ~subst context he in
+      could_reduce status ~subst context he
   | C.Appl (he::_) -> could_reduce status ~subst context he
   | C.Sort _ | C.Rel _ | C.Prod _ | C.Lambda _ | C.Const _ -> false
   | C.Appl [] | C.LetIn _ | C.Implicit _ -> assert false
@@ -412,6 +414,8 @@ and unify_for_delift status metasenv subst context t1 t2 =
    try Some
     (fo_unif_w_hints true status false true(*test_eq_only*) metasenv subst
       context (false,t1) (false,t2))
+    (*(unify status true(*test_eq_only*) metasenv subst
+      context t1 t2 false)*)
    with UnificationFailure _ | Uncertain _ | KeepReducingThis _ -> None
  in
  indent := ind; res