added simplify to avoid ugly proofterm

[helm.git] / helm / software / components / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index dd25edac4fd0531e665ebfd26e444082cf4f1e0b..ab43c3732ee6b1b572bfb66ed486ecd8439e7838 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -801,7 +801,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                     | (_,_,ty,_)::_ ->
                        fst (split_prods ~subst [] paramsno ty)
                   in
-                   (tys@lefts,List.length tl,isinductive,paramsno,cl')
+                   (lefts@tys,List.length tl,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
                   (lazy ("Unknown mutual inductive definition:" ^
@@ -852,7 +852,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                     | (_,_,ty,_)::_ ->
                        fst (split_prods ~subst [] paramsno ty)
                   in
-                   (tys@lefts,List.length tl,isinductive,paramsno,cl')
+                   (lefts@tys,List.length tl,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
                   (lazy ("Unknown mutual inductive definition:" ^
@@ -1006,7 +1006,7 @@ and guarded_by_destructors ~subst context n nn kl x safes =
                      | (_,_,ty,_)::_ ->
                         fst (split_prods ~subst [] paramsno ty)
                    in
-                    (tys@lefts,len,isinductive,paramsno,cl')
+                    (lefts@tys,len,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
                   (lazy ("Unknown mutual inductive definition:" ^
@@ -1059,7 +1059,7 @@ and guarded_by_destructors ~subst context n nn kl x safes =
                     | (_,_,ty,_)::_ ->
                        fst (split_prods ~subst [] paramsno ty)
                   in
-                   (tys@lefts,List.length tl,isinductive,paramsno,cl')
+                   (lefts@tys,List.length tl,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
                   (lazy ("Unknown mutual inductive definition:" ^
@@ -1647,6 +1647,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
    | C.LetIn (n,s,ty,t) ->
       (* only to check if s is well-typed *)
       let ty',ugraph1 = type_of_aux ~logger context s ugraph in
+      let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in
       let b,ugraph1 =
        R.are_convertible ~subst ~metasenv context ty ty' ugraph1
       in