From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 15 Jan 2009 15:33:22 +0000 (+0000)
Subject: unvariant also for coercions to funclass
X-Git-Tag: make_still_working~4255
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bee7762950741b85472b27b4818d11a51f46d861;p=helm.git

unvariant also for coercions to funclass
---

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 801e80d6c..eb350d2e5 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -131,6 +131,20 @@ let exp_impl metasenv subst context =
   | _ -> assert false
 ;;
 
+let unvariant newt =
+ 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
+;;
+
 let is_a_double_coercion t =
   let rec subst_nth n x l =
     match n,l with
@@ -1300,7 +1314,8 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                   ugraph
                 in 
                  debug_print (lazy (" has type: "^ pp tty));
-                 Some (coerc,tty,subst,metasenv,ugraph)
+
+                 Some (unvariant coerc,tty,subst,metasenv,ugraph)
               with
               | Uncertain _ | RefineFailure _
               | HExtlib.Localized (_,Uncertain _)
@@ -1452,19 +1467,7 @@ 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
+                 let newt =  unvariant newt in
                   Some ((newt,newty), subst, metasenv, ugraph)
                with 
                | Uncertain _ -> uncertain := true; None