fo_unif_l
test_equality_only subst metasenv (lr1, lr2) ugraph
with
- | UnificationFailure _
- | Uncertain _ as exn ->
+ | UnificationFailure s
+ | Uncertain s as exn ->
(match l1, l2 with
| (((Cic.Const (uri1, ens1)) as c1) :: tl1),
(((Cic.Const (uri2, ens2)) as c2) :: tl2) when
CoercGraph.is_a_coercion c1 &&
- CoercGraph.is_a_coercion c2 ->
+ CoercGraph.is_a_coercion c2 &&
+ not (UriManager.eq uri1 uri2) ->
let body1, attrs1, ugraph =
match CicEnvironment.get_obj ugraph uri1 with
| Cic.Constant (_,Some bo, _, _, attrs),u -> bo,attrs,u
| _ -> assert false
in
let is_composite1 =
- List.exists ((=) (`Class `Coercion)) attrs1 in
+ List.exists
+ (function `Class (`Coercion _) -> true | _-> false)
+ attrs1
+ in
let is_composite2 =
- List.exists ((=) (`Class `Coercion)) attrs2 in
+ List.exists
+ (function `Class (`Coercion _) -> true | _-> false)
+ attrs2
+ in
(match is_composite1, is_composite2 with
| false, false -> raise exn
| true, false ->
fo_unif_subst
test_equality_only subst context metasenv
redappl1 redappl2 ugraph)
+ (*CSC: This is necessary because of the "elim H" tactic
+ where the type of H is only reducible to an
+ inductive type. This could be extended from inductive
+ types to any rigid term. However, the code is
+ duplicated in two places: inside applications and
+ outside them. Probably it would be better to
+ work with lambda-bar terms instead. *)
+ | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
+ | (_, Cic.MutInd _::_) ->
+ let t1' = R.whd ~subst context t1 in
+ (match t1' with
+ C.Appl (C.MutInd _::_) ->
+ fo_unif_subst test_equality_only
+ subst context metasenv t1' t2 ugraph
+ | _ -> raise (UnificationFailure (lazy "88")))
+ | (Cic.MutInd _::_,_) ->
+ let t2' = R.whd ~subst context t2 in
+ (match t2' with
+ C.Appl (C.MutInd _::_) ->
+ fo_unif_subst test_equality_only
+ subst context metasenv t1 t2' ugraph
+ | _ -> raise (UnificationFailure (lazy "99")))
| _ -> raise exn)))
| (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
let subst', metasenv',ugraph1 =
in
fo_unif_subst test_equality_only subst context metasenv
beta_expanded (C.Meta (i,l)) ugraph1
+(* Works iff there are no arguments applied to it; similar to the
+ case below
+ | (_, C.MutInd _) ->
+ let t1' = R.whd ~subst context t1 in
+ (match t1' with
+ C.MutInd _ ->
+ fo_unif_subst test_equality_only
+ subst context metasenv t1' t2 ugraph
+ | _ -> raise (UnificationFailure (lazy "8")))
+*)
(* The following idea could be exploited again; right now we have no
longer any example requiring it
| (C.Prod _, t2) ->