Debugging code added.

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 25fa7ef213cbda9df38a22c95186187bce20da38..c67dc5343f622b0ce215c28c0ed5fa4dee3e99d8 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -1393,10 +1393,10 @@ and type_of_branch ~subst context argsno need_dummy outtype term constype =
           C.Appl l -> C.Appl (l@[C.Rel 1])
         | t -> C.Appl [t ; C.Rel 1]
       in
-       C.Prod (C.Anonymous,so,type_of_branch ~subst
+       C.Prod (name,so,type_of_branch ~subst
         ((Some (name,(C.Decl so)))::context) argsno need_dummy
         (CicSubstitution.lift 1 outtype) term' de)
-  | _ -> raise (AssertFailure (lazy "20"))
+   | _ -> raise (AssertFailure (lazy "20"))
 
 (* check_metasenv_consistency checks that the "canonical" context of a
 metavariable is consitent - up to relocation via the relocation list l -
@@ -1772,6 +1772,15 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
                R.are_convertible 
                  ~subst ~metasenv context ty_p ty_branch ugraph3 
              in 
+(* Debugging code
+if not b1 then
+begin
+prerr_endline ("\n!OUTTYPE= " ^ CicPp.ppterm outtype);
+prerr_endline ("!CONS= " ^ CicPp.ppterm cons);
+prerr_endline ("!TY_CONS= " ^ CicPp.ppterm ty_cons);
+prerr_endline ("#### " ^ CicPp.ppterm ty_p ^ "\n<==>\n" ^ CicPp.ppterm ty_branch);
+end;
+*)
              if not b1 then
                debug_print (lazy
                  ("#### " ^ CicPp.ppterm ty_p ^