:-(

[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 c23555494f803e279be20f54bf85c51b94c4d244..7b98a59be775fe79e02ec35f3e7e497c694554b0 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -2303,3 +2303,6 @@ let check_allowed_sort_elimination uri i s1 s2 =
   ~logger:(new CicLogger.logger) [] uri i true
   (Cic.Implicit None) (* never used *) (Cic.Sort s1) (Cic.Sort s2)
   CicUniv.empty_ugraph)
+;;
+
+Deannotate.type_of_aux' := fun context t -> fst (type_of_aux' [] context t CicUniv.oblivion_ugraph);;