more push/pop to avoid confusion with imperative data structures employed by

[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 00e40dfa6b237a63ac3a047f2c3dcbde3acd988f..30a886a2b47ad81acf62681117c04ce22e35b1c6 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -1350,6 +1350,10 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
   let module R = CicReduction in
   let module S = CicSubstitution in
   let module U = UriManager in
+(* FG: DEBUG ONLY   
+   prerr_endline ("TC: context:\n" ^ CicPp.ppcontext ~metasenv context);
+   prerr_endline ("TC: term   :\n" ^ CicPp.ppterm ~metasenv t ^ "\n");
+*)   
    match t with
       C.Rel n ->
        (try