subst context metasenv te t2 ugraph
| (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
subst context metasenv t1 te ugraph
- | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
- let subst',metasenv',ugraph1 =
- fo_unif_subst true subst context metasenv s1 s2 ugraph
- in
- fo_unif_subst test_equality_only
- subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
- | (C.Prod _, _) ->
- (match CicReduction.whd ~subst context t2 with
- | C.Prod _ as t2 ->
- fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
- | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product"))))
- | (_, C.Prod _) ->
- (match CicReduction.whd ~subst context t1 with
- | C.Prod _ as t1 ->
- fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
- | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product"))))
| (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
let subst',metasenv',ugraph1 =
fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
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) ->
- let t2' = R.whd ~subst context t2 in
- (match t2' with
- C.Prod _ ->
- fo_unif_subst test_equality_only
- subst context metasenv t1 t2' ugraph
- | _ -> raise (UnificationFailure (lazy "8")))
- | (t1, C.Prod _) ->
- let t1' = R.whd ~subst context t1 in
- (match t1' with
- C.Prod _ ->
- fo_unif_subst test_equality_only
- subst context metasenv t1' t2 ugraph
- | _ -> (* raise (UnificationFailure "9")) *)
- raise
- (UnificationFailure (lazy (sprintf
- "Can't unify %s with %s because they are not convertible"
- (CicMetaSubst.ppterm ~metasenv subst t1)
- (CicMetaSubst.ppterm ~metasenv subst t2)))))
-*)
+ | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
+ let subst',metasenv',ugraph1 =
+ fo_unif_subst true subst context metasenv s1 s2 ugraph
+ in
+ fo_unif_subst test_equality_only
+ subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
+ | (C.Prod _, _) ->
+ (match CicReduction.whd ~subst context t2 with
+ | C.Prod _ as t2 ->
+ fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
+ | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product"))))
+ | (_, C.Prod _) ->
+ (match CicReduction.whd ~subst context t1 with
+ | C.Prod _ as t1 ->
+ fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
+ | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product"))))
| (_,_) ->
(* delta-beta reduction should almost never be a problem for
unification since: