From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 29 Mar 2006 13:34:55 +0000 (+0000)
Subject: Debugging code added.
X-Git-Tag: 0.4.95@7852~1546
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a1b87ca1225a74b0d7b913e38c8ff6004737448b;p=helm.git

Debugging code added.
---

diff --git a/components/cic_proof_checking/cicTypeChecker.ml b/components/cic_proof_checking/cicTypeChecker.ml
index 25fa7ef21..c67dc5343 100644
--- a/components/cic_proof_checking/cicTypeChecker.ml
+++ b/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 ^