X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_acic%2FdoubleTypeInference.ml;h=4ca88d4b96a411318a6be88d2c6c1ef4d9e6302c;hb=7f9e313fe5ae4200f080f481a6b8b795a0618093;hp=214f656c38d5db4d27f889f9b6019b3b28d4eb12;hpb=7dc9e84cd0e40d8ff6847aabe780a4196e30be36;p=helm.git

diff --git a/helm/software/components/cic_acic/doubleTypeInference.ml b/helm/software/components/cic_acic/doubleTypeInference.ml
index 214f656c3..4ca88d4b9 100644
--- a/helm/software/components/cic_acic/doubleTypeInference.ml
+++ b/helm/software/components/cic_acic/doubleTypeInference.ml
@@ -33,20 +33,13 @@ exception WrongUriToMutualInductiveDefinitions of string;;
 exception ListTooShort;;
 exception RelToHiddenHypothesis;;
 
-let syntactic_equality_add_time = ref 0.0;;
-let type_of_aux'_add_time = ref 0.0;;
-let number_new_type_of_aux'_double_work = ref 0;;
-let number_new_type_of_aux' = ref 0;;
-let number_new_type_of_aux'_prop = ref 0;;
-
-let double_work = ref 0;;
+(*CSC: must alfa-conversion be considered or not? *)
 
 let xxx_type_of_aux' m c t =
- let t1 = Sys.time () in
- let res,_ = CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph in
- let t2 = Sys.time () in
- type_of_aux'_add_time := !type_of_aux'_add_time +. t2 -. t1 ;
- res
+ try 
+   Some (fst (CicTypeChecker.type_of_aux' m c t CicUniv.oblivion_ugraph))
+ with
+ | CicTypeChecker.TypeCheckerFailure _ -> None (* because eta_expansion *)
 ;;
 
 type types = {synthesized : Cic.term ; expected : Cic.term option};;
@@ -58,6 +51,8 @@ let rec does_not_occur n =
   function
      C.Rel m when m = n -> false
    | C.Rel _
+(* FG/CSC: maybe we assume the meta is guarded so we do not recur on its *)
+(*         explicit subsitutions (copied from the kernel) ???            *)
    | C.Meta _
    | C.Sort _
    | C.Implicit _ -> true 
@@ -69,9 +64,10 @@ let rec does_not_occur n =
    | C.Lambda (name,so,dest) ->
       does_not_occur n so &&
        does_not_occur (n + 1) dest
-   | C.LetIn (name,so,dest) ->
+   | C.LetIn (name,so,ty,dest) ->
       does_not_occur n so &&
-       does_not_occur (n + 1) dest
+       does_not_occur n ty &&
+        does_not_occur (n + 1) dest
    | C.Appl l ->
       List.fold_right (fun x i -> i && does_not_occur n x) l true
    | C.Var (_,exp_named_subst)
@@ -101,64 +97,72 @@ let rec does_not_occur n =
          ) fl true
 ;;
 
-let rec beta_reduce =
+(* FG: if ~clean:true, unreferenced letins are removed *)
+(*     (beta-reducttion can cause unreferenced letins) *)
+let rec beta_reduce ?(clean=false)=
  let module S = CicSubstitution in
  let module C = Cic in
   function
       C.Rel _ as t -> t
     | C.Var (uri,exp_named_subst) ->
        let exp_named_subst' =
-        List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
+        List.map (function (i,t) -> i, beta_reduce ~clean t) exp_named_subst
        in
         C.Var (uri,exp_named_subst')
     | C.Meta (n,l) ->
        C.Meta (n,
         List.map
-         (function None -> None | Some t -> Some (beta_reduce t)) l
+         (function None -> None | Some t -> Some (beta_reduce ~clean t)) l
        )
     | C.Sort _ as t -> t
     | C.Implicit _ -> assert false
     | C.Cast (te,ty) ->
-       C.Cast (beta_reduce te, beta_reduce ty)
+       C.Cast (beta_reduce ~clean te, beta_reduce ~clean ty)
     | C.Prod (n,s,t) ->
-       C.Prod (n, beta_reduce s, beta_reduce t)
+       C.Prod (n, beta_reduce ~clean s, beta_reduce ~clean t)
     | C.Lambda (n,s,t) ->
-       C.Lambda (n, beta_reduce s, beta_reduce t)
-    | C.LetIn (n,s,t) ->
-       C.LetIn (n, beta_reduce s, beta_reduce t)
+       C.Lambda (n, beta_reduce ~clean s, beta_reduce ~clean t)
+    | C.LetIn (n,s,ty,t) ->
+       let t' = beta_reduce ~clean t in
+       if clean && does_not_occur 1 t' then
+	  (* since [Rel 1] does not occur in typ, substituting any term *)
+          (* in place of [Rel 1] is equivalent to delifting once        *)
+          CicSubstitution.subst (C.Implicit None) t'
+       else
+          C.LetIn (n, beta_reduce ~clean s, beta_reduce ~clean ty, t')
     | C.Appl ((C.Lambda (name,s,t))::he::tl) ->
        let he' = S.subst he t in
         if tl = [] then
-         beta_reduce he'
+         beta_reduce ~clean he'
         else
          (match he' with
-             C.Appl l -> beta_reduce (C.Appl (l@tl))
-           | _ -> beta_reduce (C.Appl (he'::tl)))
+             C.Appl l -> beta_reduce ~clean (C.Appl (l@tl))
+           | _ -> beta_reduce ~clean (C.Appl (he'::tl)))
     | C.Appl l ->
-       C.Appl (List.map beta_reduce l)
+       C.Appl (List.map (beta_reduce ~clean) l)
     | C.Const (uri,exp_named_subst) ->
        let exp_named_subst' =
-        List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
+        List.map (function (i,t) -> i, beta_reduce ~clean t) exp_named_subst
        in
         C.Const (uri,exp_named_subst')
     | C.MutInd (uri,i,exp_named_subst) ->
        let exp_named_subst' =
-        List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
+        List.map (function (i,t) -> i, beta_reduce ~clean t) exp_named_subst
        in
         C.MutInd (uri,i,exp_named_subst')
     | C.MutConstruct (uri,i,j,exp_named_subst) ->
        let exp_named_subst' =
-        List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
+        List.map (function (i,t) -> i, beta_reduce ~clean t) exp_named_subst
        in
         C.MutConstruct (uri,i,j,exp_named_subst')
     | C.MutCase (sp,i,outt,t,pl) ->
-       C.MutCase (sp,i,beta_reduce outt,beta_reduce t,
-        List.map beta_reduce pl)
+       C.MutCase (sp,i,beta_reduce ~clean outt,beta_reduce ~clean t,
+        List.map (beta_reduce ~clean) pl)
     | C.Fix (i,fl) ->
        let fl' =
         List.map
          (function (name,i,ty,bo) ->
-           name,i,beta_reduce ty,beta_reduce bo
+           name,i,beta_reduce ~clean ty,beta_reduce ~clean bo
          ) fl
        in
         C.Fix (i,fl')
@@ -166,90 +170,12 @@ let rec beta_reduce =
        let fl' =
         List.map
          (function (name,ty,bo) ->
-           name,beta_reduce ty,beta_reduce bo
+           name,beta_reduce ~clean ty,beta_reduce ~clean bo
          ) fl
        in
         C.CoFix (i,fl')
 ;;
 
-(* syntactic_equality up to the                 *)
-(* distinction between fake dependent products  *)
-(* and non-dependent products, alfa-conversion  *)
-(*CSC: must alfa-conversion be considered or not? *)
-let syntactic_equality t t' =
- let module C = Cic in
- let rec syntactic_equality t t' =
-  if t = t' then true
-  else
-   match t, t' with
-      C.Var (uri,exp_named_subst), C.Var (uri',exp_named_subst') ->
-       UriManager.eq uri uri' &&
-        syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
-    | C.Cast (te,ty), C.Cast (te',ty') ->
-       syntactic_equality te te' &&
-        syntactic_equality ty ty'
-    | C.Prod (_,s,t), C.Prod (_,s',t') ->
-       syntactic_equality s s' &&
-        syntactic_equality t t'
-    | C.Lambda (_,s,t), C.Lambda (_,s',t') ->
-       syntactic_equality s s' &&
-        syntactic_equality t t'
-    | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
-       syntactic_equality s s' &&
-        syntactic_equality t t'
-    | C.Appl l, C.Appl l' ->
-       List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l'
-    | C.Const (uri,exp_named_subst), C.Const (uri',exp_named_subst') ->
-       UriManager.eq uri uri' &&
-        syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
-    | C.MutInd (uri,i,exp_named_subst), C.MutInd (uri',i',exp_named_subst') ->
-       UriManager.eq uri uri' && i = i' &&
-        syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
-    | C.MutConstruct (uri,i,j,exp_named_subst),
-      C.MutConstruct (uri',i',j',exp_named_subst') ->
-       UriManager.eq uri uri' && i = i' && j = j' &&
-        syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
-    | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') ->
-       UriManager.eq sp sp' && i = i' &&
-        syntactic_equality outt outt' &&
-         syntactic_equality t t' &&
-          List.fold_left2
-           (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl'
-    | C.Fix (i,fl), C.Fix (i',fl') ->
-       i = i' &&
-        List.fold_left2
-         (fun b (_,i,ty,bo) (_,i',ty',bo') ->
-           b && i = i' &&
-            syntactic_equality ty ty' &&
-             syntactic_equality bo bo') true fl fl'
-    | C.CoFix (i,fl), C.CoFix (i',fl') ->
-       i = i' &&
-        List.fold_left2
-         (fun b (_,ty,bo) (_,ty',bo') ->
-           b &&
-            syntactic_equality ty ty' &&
-             syntactic_equality bo bo') true fl fl'
-    | _, _ -> false (* we already know that t != t' *)
- and syntactic_equality_exp_named_subst exp_named_subst1 exp_named_subst2 =
-  List.fold_left2
-   (fun b (_,t1) (_,t2) -> b && syntactic_equality t1 t2) true
-   exp_named_subst1 exp_named_subst2
- in
-  try
-   syntactic_equality t t'
-  with
-   _ -> false
-;;
-
-let xxx_syntactic_equality t t' =
- let t1 = Sys.time () in
- let res = syntactic_equality t t' in
- let t2 = Sys.time () in
- syntactic_equality_add_time := !syntactic_equality_add_time +. t2 -. t1 ;
- res
-;;
-
-
 let rec split l n =
  match (l,n) with
     (l,0) -> ([], l)
@@ -262,9 +188,9 @@ let type_of_constant uri =
  let module R = CicReduction in
  let module U = UriManager in
   let cobj =
-   match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
+   match CicEnvironment.is_type_checked CicUniv.oblivion_ugraph uri with
       CicEnvironment.CheckedObj (cobj,_) -> cobj
-    | CicEnvironment.UncheckedObj uobj ->
+    | CicEnvironment.UncheckedObj (uobj,_) ->
        raise (NotWellTyped "Reference to an unchecked constant")
   in
    match cobj with
@@ -277,9 +203,9 @@ let type_of_variable uri =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
-  match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
+  match CicEnvironment.is_type_checked CicUniv.oblivion_ugraph uri with
      CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),_) -> ty
-   | CicEnvironment.UncheckedObj (C.Variable _) ->
+   | CicEnvironment.UncheckedObj (C.Variable _,_) ->
       raise (NotWellTyped "Reference to an unchecked variable")
    |  _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
 ;;
@@ -289,9 +215,9 @@ let type_of_mutual_inductive_defs uri i =
  let module R = CicReduction in
  let module U = UriManager in
   let cobj =
-   match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
+   match CicEnvironment.is_type_checked CicUniv.oblivion_ugraph uri with
       CicEnvironment.CheckedObj (cobj,_) -> cobj
-    | CicEnvironment.UncheckedObj uobj ->
+    | CicEnvironment.UncheckedObj (uobj,_) ->
        raise (NotWellTyped "Reference to an unchecked inductive type")
   in
    match cobj with
@@ -306,9 +232,9 @@ let type_of_mutual_inductive_constr uri i j =
  let module R = CicReduction in
  let module U = UriManager in
   let cobj =
-   match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
+   match CicEnvironment.is_type_checked CicUniv.oblivion_ugraph uri with
       CicEnvironment.CheckedObj (cobj,_) -> cobj
-    | CicEnvironment.UncheckedObj uobj ->
+    | CicEnvironment.UncheckedObj (uobj,_) ->
        raise (NotWellTyped "Reference to an unchecked constructor")
   in
    match cobj with
@@ -321,6 +247,18 @@ let type_of_mutual_inductive_constr uri i j =
 
 let pack_coercion = ref (fun _ _ _ -> assert false);;
 
+let profiler_for_find = HExtlib.profile "CicHash ADD" ;;
+
+let cic_CicHash_add a b c =  
+  profiler_for_find.HExtlib.profile (Cic.CicHash.add a b) c
+;;
+
+let profiler_for_find1 = HExtlib.profile "CicHash MEM" ;;
+
+let cic_CicHash_mem a b =  
+  profiler_for_find1.HExtlib.profile (Cic.CicHash.mem a) b
+;;
+
 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
 let rec type_of_aux' subterms_to_types metasenv context t expectedty =
  (* Coscoy's double type-inference algorithm             *)
@@ -342,10 +280,8 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
         (try
           match List.nth context (n - 1) with
              Some (_,C.Decl t) -> S.lift n t
-           | Some (_,C.Def (_,Some ty)) -> S.lift n ty
-           | Some (_,C.Def (bo,None)) ->
-              type_of_aux context (S.lift n bo) expectedty
-	         | None -> raise RelToHiddenHypothesis
+           | Some (_,C.Def (_,ty)) -> S.lift n ty
+	   | None -> raise RelToHiddenHypothesis
          with
           _ -> raise (NotWellTyped "Not a close term")
         )
@@ -361,11 +297,12 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
               [] -> []
             | (Some (n,C.Decl t))::tl ->
                (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
-            | (Some (n,C.Def (t,None)))::tl ->
-               (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::
-                (aux (i+1) tl)
+            | (Some (n,C.Def (t,ty)))::tl ->
+               (Some (n,
+                C.Def
+                 ((S.subst_meta l (S.lift i t)),S.subst_meta l (S.lift i t))))::
+                  (aux (i+1) tl)
             | None::tl -> None::(aux (i+1) tl)
-            | (Some (_,C.Def (_,Some _)))::_ -> assert false
           in
            aux 1 canonical_context
          in
@@ -376,14 +313,15 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
                  _,None -> ()
                | Some t,Some (_,C.Def (ct,_)) ->
                   let expected_type =
-                   R.whd context
-                    (xxx_type_of_aux' metasenv context ct)
+                    match xxx_type_of_aux' metasenv context ct with
+                    | None -> None
+                    | Some t -> Some (R.whd context t)
                   in
                    (* Maybe I am a bit too paranoid, because   *)
                    (* if the term is well-typed than t and ct  *)
                    (* are convertible. Nevertheless, I compute *)
                    (* the expected type.                       *)
-                   ignore (type_of_aux context t (Some expected_type))
+                   ignore (type_of_aux context t expected_type)
                | Some t,Some (_,C.Decl ct) ->
                   ignore (type_of_aux context t (Some ct))
                | _,_ -> assert false (* the term is not well typed!!! *)
@@ -409,38 +347,40 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
      | C.Lambda (n,s,t) ->
         (* Let's visit all the subterms that will not be visited later *)
          let _ = type_of_aux context s None in 
-         let expected_target_type =
+         let n, expected_target_type =
           match expectedty with
-             None -> None
+           | None -> n, None
            | Some expectedty' ->
-              let ty =
+              let n, ty =
                match R.whd context expectedty' with
-                  C.Prod (_,_,expected_target_type) ->
-                   beta_reduce expected_target_type
+                | C.Prod (n',_,expected_target_type) ->
+                   let xtt = beta_reduce expected_target_type in
+		   if n <> C.Anonymous then n, xtt else n', xtt
                 | _ -> assert false
               in
-               Some ty
+               n, Some ty
          in 
           let type2 =
            type_of_aux ((Some (n,(C.Decl s)))::context) t expected_target_type
           in
            (* Checks suppressed *)
            C.Prod (n,s,type2)
-     | C.LetIn (n,s,t) ->
+     | C.LetIn (n,s,ty,t) ->
 (*CSC: What are the right expected types for the source and *)
 (*CSC: target of a LetIn? None used.                        *)
         (* Let's visit all the subterms that will not be visited later *)
-        let ty = type_of_aux context s None in
+        let _ = type_of_aux context ty None in
+        let _ = type_of_aux context s (Some ty) in
          let t_typ =
           (* Checks suppressed *)
-          type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t None
+          type_of_aux ((Some (n,(C.Def (s,ty))))::context) t None
          in  (* CicSubstitution.subst s t_typ *)
-          if does_not_occur 1 t_typ then
-           (* since [Rel 1] does not occur in typ, substituting any term *)
+	  if does_not_occur 1 t_typ then
+	   (* since [Rel 1] does not occur in typ, substituting any term *)
            (* in place of [Rel 1] is equivalent to delifting once        *)
            CicSubstitution.subst (C.Implicit None) t_typ
           else
-           C.LetIn (n,s,t_typ)
+           C.LetIn (n,s,ty,t_typ)
      | C.Appl (he::tl) when List.length tl > 0 ->
         (* 
         let expected_hetype =
@@ -510,11 +450,12 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
         in
         let (parameters, arguments,exp_named_subst) =
          let type_of_term =
-          xxx_type_of_aux' metasenv context term
+           match xxx_type_of_aux' metasenv context term with
+           | None -> None
+           | Some t -> Some (beta_reduce t)
          in
           match
-           R.whd context (type_of_aux context term
-            (Some (beta_reduce type_of_term)))
+           R.whd context (type_of_aux context term type_of_term)
           with
              (*CSC manca il caso dei CAST *)
              C.MutInd (uri',i',exp_named_subst) ->
@@ -532,7 +473,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
          let (cl,parsno) =
            let obj,_ =
              try
-               CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+               CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
              with Not_found -> assert false
            in
           match obj with
@@ -551,11 +492,15 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
                 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
               in
                let expectedtype =
-                type_of_branch context parsno need_dummy outtype cons
-                  (xxx_type_of_aux' metasenv context cons)
+                 match xxx_type_of_aux' metasenv context cons with
+                 | None -> None
+                 | Some t -> 
+                     Some 
+                       (beta_reduce 
+                         (type_of_branch context parsno need_dummy outtype 
+                           cons t))
                in
-                ignore (type_of_aux context p
-                 (Some (beta_reduce expectedtype))) ;
+                ignore (type_of_aux context p expectedtype);
                 j+1
             ) 1 (List.combine pl cl)
           in
@@ -614,14 +559,15 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
           let (_,ty,_) = List.nth fl i in
            ty
    in
-    let synthesized' = beta_reduce synthesized in
+(* FG: beta-reduction can cause unreferenced letins *)
+    let synthesized' = beta_reduce ~clean:true synthesized in
     let synthesized' = !pack_coercion metasenv context synthesized' in
      let types,res =
       match expectedty with
          None ->
           (* No expected type *)
           {synthesized = synthesized' ; expected = None}, synthesized
-       | Some ty when xxx_syntactic_equality synthesized' ty ->
+       | Some ty when CicUtil.alpha_equivalence synthesized' ty ->
           (* The expected type is synthactically equal to *)
           (* the synthesized type. Let's forget it.       *)
           {synthesized = synthesized' ; expected = None}, synthesized
@@ -629,15 +575,15 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
           {synthesized = synthesized' ; expected = Some expectedty'},
           expectedty'
      in
-      assert (not (Cic.CicHash.mem subterms_to_types t));
-      Cic.CicHash.add subterms_to_types t types ;
+(*      assert (not (cic_CicHash_mem subterms_to_types t));*)
+      cic_CicHash_add subterms_to_types t types ;
       res
 
  and visit_exp_named_subst context uri exp_named_subst =
   let uris_and_types =
      let obj,_ =
        try
-         CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+         CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
        with Not_found -> assert false
      in
     let params = CicUtil.params_of_obj obj in
@@ -645,7 +591,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
       (function uri ->
          let obj,_ =
            try
-             CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+             CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
            with Not_found -> assert false
          in
          match obj with
@@ -655,7 +601,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
   in
    let rec check uris_and_types subst =
     match uris_and_types,subst with
-       _,[] -> []
+       _,[] -> ()
      | (uri,ty)::tytl,(uri',t)::substtl when uri = uri' ->
         ignore (type_of_aux context t (Some ty)) ;
         let tytl' =
@@ -672,15 +618,10 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
    let t1' = CicReduction.whd context t1 in
    let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
    match (t1', t2') with
-      (C.Sort _, C.Sort s2)
-        when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> 
-	 (* different from Coq manual!!! *)
-         C.Sort s2
-    | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> 
-	C.Sort (C.Type (CicUniv.fresh()))
-    | (C.Sort _,C.Sort (C.Type t1)) -> 
-        (* TASSI: CONSRTAINTS: the same in cictypechecker,cicrefine *)
-	C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *)
+    | (C.Sort _, C.Sort s2) when (s2 = C.Prop || s2 = C.Set) -> C.Sort s2
+    | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->C.Sort(C.Type(CicUniv.fresh()))
+    | (C.Sort _,C.Sort (C.Type t1)) -> C.Sort (C.Type t1)
+    | (C.Sort _,C.Sort (C.CProp t1)) -> C.Sort (C.CProp t1)
     | (C.Meta _, C.Sort _) -> t2'
     | (C.Meta _, (C.Meta (_,_) as t))
     | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->