sort_of_prod changed to not generate a new metavariable in the case Meta vs

Sort. Reason: the new metavariable is not constrained in any way and, at the
end, we find it in the final metasenv.

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 60b6129b1c2db4ca806e4460872e95db635f525d..ee5916e0c50a54276fdc2b51fbe1fd48264ead03 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -188,7 +188,8 @@ and type_of_aux' metasenv context t =
        let sort2,subst'',metasenv'' =
         type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t
        in
-        sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
+        sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2),
+         subst'',metasenv''
    | C.Lambda (n,s,t) ->
        let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
        let type2,subst'',metasenv'' =
@@ -198,10 +199,10 @@ and type_of_aux' metasenv context t =
          type_of_aux subst'' metasenv''((Some (n,(C.Decl s)))::context) type2
         in
          (* only to check if the product is well-typed *)
-         let _,subst'''',metasenv'''' =
+         let _ =
           sort_of_prod subst''' metasenv''' context (n,s) (sort1,sort2)
          in
-          C.Prod (n,s,type2),subst'''',metasenv''''
+          C.Prod (n,s,type2),subst''',metasenv'''
    | C.LetIn (n,s,t) ->
       (* only to check if s is well-typed *)
       let ty,subst',metasenv' = type_of_aux subst metasenv context s in
@@ -466,21 +467,17 @@ and type_of_aux' metasenv context t =
     match (t1'', t2'') with
        (C.Sort s1, C.Sort s2)
          when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
-          C.Sort s2,subst,metasenv
+          C.Sort s2
      | (C.Sort s1, C.Sort s2) ->
          (*CSC manca la gestione degli universi!!! *)
-         C.Sort C.Type,subst,metasenv
+         C.Sort C.Type
      | (C.Meta _,_) | (_,C.Meta _) ->
          (* TODO how can we force the meta to become a sort? If we don't we
           * brake the invariant that refine produce only well typed terms *)
          (* TODO if we check the non meta term and if it is a sort then we are
           * likely to know the exact value of the result e.g. if the rhs is a
           * Sort (Prop | Set | CProp) then the result is the rhs *)
-         let (metasenv, idx) = CicMkImplicit.mk_implicit metasenv context in
-         let irl =
-           CicMkImplicit.identity_relocation_list_for_metavariable context
-         in
-         C.Meta (idx, irl), subst, metasenv
+          t2''
      | (_,_) ->
          raise (NotRefinable (sprintf
           "Two types were expected, found %s (that reduces to %s) and %s (that reducecs to %s)"