is_really_smaller in sync with old kernel, impossible cases removed

diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml
index 6e2074db0b887120901a5429865567afe84cdc2b..b65057e37bd6b667e6aaa66eb6608e3c2df391b8 100644 (file)
--- a/helm/software/components/ng_kernel/check.ml
+++ b/helm/software/components/ng_kernel/check.ml
@@ -63,7 +63,11 @@ let _ =
   CicEnvironment.set_trust (fun _ -> false);
   List.iter (fun u ->
           prerr_endline (" - " ^ UriManager.string_of_uri u);
+          try
           ignore(CicTypeChecker.typecheck u);
+          with 
+          | CicTypeChecker.AssertFailure s
+          | CicTypeChecker.TypeCheckerFailure s -> prerr_endline (Lazy.force s)
     ) alluris;
   prerr_endline "loading...";
   List.iter 

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 690cd59005f8334a9789b58d4e019102cd64786f..76bedd833bebcbe97d70c6ba9a28a118e9bff3c6 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -1013,17 +1013,10 @@ and split_prods ~subst context n te =
 and is_really_smaller ~subst ~metasenv (context, recfuns, x, safes as k) te =
  match R.whd ~subst context te with
  | C.Rel m when List.mem m safes -> true
- | C.Rel _ -> false
- | C.LetIn _ -> raise (AssertFailure (lazy "letin after whd"))
- | C.Sort _ | C.Implicit _ | C.Prod _ | C.Lambda _ 
- | C.Const (Ref.Ref (_,_,(Ref.Decl | Ref.Def | Ref.Ind _ | Ref.CoFix _))) ->
-    raise (AssertFailure (lazy "not a constructor"))
- | C.Appl ([]|[_]) -> raise (AssertFailure (lazy "empty/unary appl"))
- | C.Appl (he::_) ->
-    (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
-    (*CSC: solo perche' non abbiamo trovato controesempi            *)
-    (*TASSI: da capire soprattutto se he è un altro fix che non ha ridotto...*)
-    is_really_smaller ~subst ~metasenv k he
+ | C.Lambda (name, s, t) ->
+     is_really_smaller ~subst ~metasenv (shift_k (name, C.Decl s) k) t
+ | C.Rel _ 
+ | C.Appl _
  | C.Const (Ref.Ref (_,_,Ref.Con _)) -> false
  | C.Const (Ref.Ref (_,_,Ref.Fix _)) -> assert false
    (*| C.Fix (_, fl) ->
@@ -1044,9 +1037,7 @@ and is_really_smaller ~subst ~metasenv (context, recfuns, x, safes as k) te =
             is_really_smaller ~subst (tys@context) n_plus_len nn_plus_len kl
              x_plus_len safes' bo
          ) fl true*)
- | C.Meta _ -> 
-     true (* XXX if this check is repeated when the user completes the
-             definition *)
+ | C.Meta _ -> true 
  | C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) ->
     (match term with
     | C.Rel m | C.Appl (C.Rel m :: _ ) when List.mem m safes || m = x ->
@@ -1062,6 +1053,7 @@ and is_really_smaller ~subst ~metasenv (context, recfuns, x, safes as k) te =
              is_really_smaller ~subst ~metasenv k e)
            pl cl
     | _ -> List.for_all (is_really_smaller ~subst ~metasenv k) pl)
+ | _ -> assert false
 
 and returns_a_coinductive ~subst context ty =
   match R.whd ~subst context ty with