From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 15 Jan 2009 11:07:37 +0000 (+0000)
Subject: coercions that are marked as variant are unfolded when inserted
X-Git-Tag: make_still_working~4258
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=16770c377b03dd7690dd2d2533a4981f097ba93b;hp=e79fd328fe626dbd8c76183c36f721119e9fb668;p=helm.git

coercions that are marked as variant are unfolded when inserted
---

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 7b472a851..801e80d6c 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1452,6 +1452,19 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                 if b then 
                   Some ((t,infty), subst, metasenv, ugraph)
                 else 
+                 let newt =  (* unfold coercion if `Variant *)
+                  match newt with
+                  | Cic.Appl (hd::args) ->
+                     let uri = CicUtil.uri_of_term hd in
+                     (match 
+                       CicEnvironment.get_obj CicUniv.oblivion_ugraph uri 
+                     with
+                     | Cic.Constant (_,Some t,_,[],attrs),_ 
+                       when List.exists ((=) (`Flavour `Variant)) attrs -> 
+                        Cic.Appl (t::args)
+                     | _ -> newt)
+                  | _ -> newt
+                 in
                   Some ((newt,newty), subst, metasenv, ugraph)
                with 
                | Uncertain _ -> uncertain := true; None