From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 26 Jul 2006 15:50:54 +0000 (+0000)
Subject: Patch to the unification to make the case (i l) vs (t l) work when i is
X-Git-Tag: 0.4.95@7852~1144
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b934a94a5d005f9d8e668ef49ec83487090a787b;p=helm.git

Patch to the unification to make the case (i l) vs (t l) work when i is
an inductive type and (t l) must be subject to weak head reduction.
---

diff --git a/components/cic_unification/cicUnification.ml b/components/cic_unification/cicUnification.ml
index 437d541ea..44712199e 100644
--- a/components/cic_unification/cicUnification.ml
+++ b/components/cic_unification/cicUnification.ml
@@ -625,6 +625,28 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
                           fo_unif_subst 
                             test_equality_only subst context metasenv 
                              redappl1 redappl2 ugraph)
+                  (*CSC: This is necessary because of the "elim H" tactic
+                         where the type of H is only reducible to an
+                         inductive type. This could be extended from inductive
+                         types to any rigid term. However, the code is
+                         duplicated in two places: inside applications and
+                         outside them. Probably it would be better to
+                         work with lambda-bar terms instead. *)
+                  | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
+                  | (_, Cic.MutInd _::_) ->
+                     let t1' = R.whd ~subst context t1 in
+                     (match t1' with
+                          C.Appl (C.MutInd _::_) -> 
+                            fo_unif_subst test_equality_only 
+                              subst context metasenv t1' t2 ugraph         
+                        | _ -> raise (UnificationFailure (lazy "88")))
+                  | (Cic.MutInd _::_,_) ->
+                     let t2' = R.whd ~subst context t2 in
+                     (match t2' with
+                          C.Appl (C.MutInd _::_) -> 
+                            fo_unif_subst test_equality_only 
+                              subst context metasenv t1 t2' ugraph         
+                        | _ -> raise (UnificationFailure (lazy "99")))
                   | _ -> raise exn)))
    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
        let subst', metasenv',ugraph1 = 
@@ -669,6 +691,16 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
        in
          fo_unif_subst test_equality_only subst context metasenv 
            beta_expanded (C.Meta (i,l)) ugraph1
+(* Works iff there are no arguments applied to it; similar to the
+   case below
+   | (_, C.MutInd _) ->
+       let t1' = R.whd ~subst context t1 in
+       (match t1' with
+            C.MutInd _ -> 
+              fo_unif_subst test_equality_only 
+                subst context metasenv t1' t2 ugraph         
+          | _ -> raise (UnificationFailure (lazy "8")))
+*)
 (* The following idea could be exploited again; right now we have no
    longer any example requiring it
    | (C.Prod _, t2) ->