1. is_meta_closed should be applied only to terms on which a substitution

[helm.git] / helm / software / components / cic_unification / cicRefine.ml

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 21af1f9c74533cb640311e630c61fac70ffa0f96..8ae5964c9cf209a8ba43ea65a1c9efcbd0329b40 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -505,8 +505,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
               t' sort2 subst'' context_for_t metasenv'' ugraph2
             in
               let sop,subst''',metasenv''',ugraph3 =
-                sort_of_prod subst'' metasenv'' 
-                  context (name,s') (sort1,sort2) ugraph2
+                sort_of_prod localization_tbl subst'' metasenv'' 
+                  context (name,s') t' (sort1,sort2) ugraph2
               in
                 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
         | C.Lambda (n,s,t) ->
@@ -1136,7 +1136,9 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
       check_exp_named_subst_aux metasubst metasenv [] tl ugraph
 
 
-  and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
+  and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
+   ugraph
+  =
     let module C = Cic in
     let context_for_t2 = (Some (name,C.Decl s))::context in
     let t1'' = CicReduction.whd ~subst context t1 in
@@ -1172,15 +1174,23 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
              with _ -> assert false (* unification against a metavariable *)
             in
               t2'',subst,metasenv,ugraph1
+        | (C.Sort _,_)
+        | (C.Meta _,_) -> 
+            enrich localization_tbl s
+             (RefineFailure 
+               (lazy 
+                 (sprintf
+                   "%s is supposed to be a type, but its type is %s"
+               (CicMetaSubst.ppterm_in_context subst t context)
+               (CicMetaSubst.ppterm_in_context subst t2 context))))
         | _,_ -> 
-            raise 
-              (RefineFailure 
-                (lazy 
-                  (sprintf
-                    ("Two sorts were expected, found %s " ^^ 
-                     "(that reduces to %s) and %s (that reduces to %s)")
-                (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
-                (CicPp.ppterm t2''))))
+            enrich localization_tbl t
+             (RefineFailure 
+               (lazy 
+                 (sprintf
+                   "%s is supposed to be a type, but its type is %s"
+               (CicMetaSubst.ppterm_in_context subst s context)
+               (CicMetaSubst.ppterm_in_context subst t1 context))))
 
   and avoid_double_coercion context subst metasenv ugraph t ty = 
    if not !pack_coercions then
@@ -1500,7 +1510,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
     in
     (* first we check if we are in the simple case of a meta closed term *)
     let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
-     if CicUtil.is_meta_closed hetype then
+     if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
       (* this optimization is to postpone fix_arity (the most common case)*)
       subst,metasenv,ugraph,hetype,he,args_bo_and_ty
      else