sort_of_prod now thinks that a "sort metavariable" is a metavariable where

no free variable occurs in the local context. Reason: there used to be a bug
induced by the fact that a metavariable ?1 with an empty canonical context
could be istantiated with a metavariable ?2[l] where l has no free variables
but still it is not of length 0.

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 8403f5f0c082e295da72e48c1764cd27adc24ea2..9c9c0e58cd0dd2a9428d1c967ba272d619685a34 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -203,7 +203,7 @@ and does_not_occur context n nn te =
    match CicReduction.whd context te with
       C.Rel m when m > n && m <= nn -> false
     | C.Rel _
-    | C.Meta _
+    | C.Meta _  (* CSC: Are we sure? No recursion?*)
     | C.Sort _
     | C.Implicit _ -> true
     | C.Cast (te,ty) ->
@@ -1294,7 +1294,8 @@ and check_metasenv_consistency metasenv context canonical_context l =
       | (Some (n,C.Def (t,None)))::tl ->
          (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
       | None::tl -> None::(aux (i+1) tl)
-      | (Some (n,C.Def (_,Some _)))::_ -> assert false
+      | (Some (n,C.Def (t,Some ty)))::tl ->
+         (Some (n,C.Def ((S.lift_meta l (S.lift i t)),Some (S.lift_meta l (S.lift i ty)))))::(aux (i+1) tl)
     in
      aux 1 canonical_context
    in
@@ -1638,8 +1639,9 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^
          C.Sort s2
     | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
     | (C.Meta _, C.Sort _) -> t2'
-    | (C.Meta _, C.Meta (_,[]))
-    | (C.Sort _, C.Meta (_,[])) -> t2'
+    | (C.Meta _, (C.Meta (_,_) as t))
+    | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
+        t2'
     | (_,_) -> raise (TypeCheckerFailure (sprintf
         "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
           (CicPp.ppterm t2')))