List.map
(function
(m,canonical_context,ty) when m = metano ->
- let canonical_context' =
+ let context_changed, canonical_context' =
List.fold_right
- (fun entry context ->
+ (fun entry (b, context) ->
match entry with
- Some (Cic.Name hyp',_) when hyp' = hyp -> None::context
- | None -> None::context
+ Some (Cic.Name hyp',_) when hyp' = hyp ->
+ (true, None::context)
+ | None -> (b, None::context)
| Some (_,Cic.Def (_,Some _)) -> assert false
| Some (n,C.Decl t)
| Some (n,C.Def (t,None)) ->
- 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, [])
in
- let _,_ =
+ if not context_changed then
+ raise (Fail ("Hypothesis " ^ hyp ^ " does not exist"));
+ let _,_ =
try
CicTypeChecker.type_of_aux' metasenv canonical_context' ty
- CicUniv.empty_ugraph (* TASSI: FIXME *)
+ CicUniv.empty_ugraph
with _ ->
raise (Fail ("Hypothesis " ^ hyp ^ " occurs in the goal"))
in