From 234daa5c3bb5fd17a5dda949692b80d79d7e8ab3 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 5 Dec 2001 11:46:13 +0000 Subject: [PATCH] Just code clean-up. --- helm/ocaml/cic_proof_checking/cicReduction.ml | 4 +++- .../cic_proof_checking/cicTypeChecker.ml | 19 +++++++++---------- 2 files changed, 12 insertions(+), 11 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml index e0ad91f59..395d7a696 100644 --- a/helm/ocaml/cic_proof_checking/cicReduction.ml +++ b/helm/ocaml/cic_proof_checking/cicReduction.ml @@ -202,7 +202,7 @@ let are_convertible t1 t2 = let t1' = whd t1 and t2' = whd t2 in debug t1' [t2'] "POSTWHD"; - (*if !fdebug = 0 then ignore(Unix.system "read" );*) +let res = match (t1',t2') with (C.Rel n1, C.Rel n2) -> n1 = n2 | (C.Var uri1, C.Var uri2) -> U.eq uri1 uri2 @@ -262,6 +262,8 @@ let are_convertible t1 t2 = | (_,_) -> debug t1' [t2'] "NOT-CONVERTIBLE" ; false +in +if res then true else (debug t1' [t2'] "NOT-CONVERTIBLE" ; false) end in aux t1 t2 diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index f33d56e1b..77a125160 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -1019,9 +1019,7 @@ and type_of_aux' env t = | C.Appl (he::tl) when List.length tl > 0 -> let hetype = type_of_aux env he and tlbody_and_type = List.map (fun x -> (x, type_of_aux env x)) tl in - (try - eat_prods hetype tlbody_and_type - with _ -> debug (C.Appl (he::tl)) env ; C.Implicit) + eat_prods hetype tlbody_and_type | C.Appl _ -> raise (NotWellTyped "Appl: no arguments") | C.Const (uri,cookingsno) -> incr fdebug ; @@ -1196,15 +1194,16 @@ and type_of_aux' env t = Cic.Prod (n,s,t) -> if CicReduction.are_convertible s hety then (CicReduction.fdebug := -1 ; - eat_prods (CicSubstitution.subst hete t) tl + eat_prods (CicSubstitution.subst hete t) tl ) else - ( - CicReduction.fdebug := 0 ; - let _ = CicReduction.are_convertible s hety in - debug hete [hety ; s] ; - raise (NotWellTyped "Appl: wrong parameter-type") -) + begin + CicReduction.fdebug := 0 ; + ignore (CicReduction.are_convertible s hety) ; + fdebug := 0 ; + debug s [hety] ; + raise (NotWellTyped "Appl: wrong parameter-type") + end | _ -> raise (NotWellTyped "Appl: wrong Prod-type") ) in -- 2.39.2