From 16770c377b03dd7690dd2d2533a4981f097ba93b Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 15 Jan 2009 11:07:37 +0000
Subject: [PATCH] coercions that are marked as variant are unfolded when
 inserted

---
 .../components/cic_unification/cicRefine.ml         | 13 +++++++++++++
 1 file changed, 13 insertions(+)

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
-- 
2.39.2