From a1b87ca1225a74b0d7b913e38c8ff6004737448b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 29 Mar 2006 13:34:55 +0000 Subject: [PATCH] Debugging code added. --- components/cic_proof_checking/cicTypeChecker.ml | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) 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 ^ -- 2.39.2