- let _,_ =
- try
- CicTypeChecker.type_of_aux' metasenv context t
- CicUniv.empty_ugraph (* TASSI: FIXME *)
- with _ ->
- raise
- (Fail
- ("Hypothesis " ^ string_of_name n ^
- " uses hypothesis " ^ hyp))
- in
- entry::context
- ) canonical_context []
+ if b then
+ let _,_ =
+ try
+ CicTypeChecker.type_of_aux' metasenv context t
+ CicUniv.empty_ugraph
+ with _ ->
+ raise
+ (Fail
+ ("Hypothesis " ^ string_of_name n ^
+ " uses hypothesis " ^ hyp))
+ in
+ (b, entry::context)
+ else
+ (b, entry::context)
+ ) canonical_context (false, [])