(CicMetaSubst.ppmetasenv metasenv subst)
(CicMetaSubst.ppsubst subst) msg) in
raise (AssertFailure msg);;
-(*
->>>>>>> 1.40
- try
- CicMetaSubst.type_of_aux' metasenv subst context term ugraph
- with
- | CicMetaSubst.MetaSubstFailure msg ->
- raise (AssertFailure
- ((sprintf
- "Type checking error: %s in context\n%s\nand metasenv\n%s.\nException: %s.\nBroken invariant: unification must be invoked only on well typed terms"
- (CicMetaSubst.ppterm subst term)
- (CicMetaSubst.ppcontext subst context)
- (CicMetaSubst.ppmetasenv metasenv subst) msg))) *)
let rec deref subst =
let snd (_,a,_) = a in
fo_unif_subst test_equality_only subst context metasenv
(C.Meta (i,l)) beta_expanded ugraph1)
| _,_ ->
-(* WAS BEFORE -----
-<<<<<<< cicUnification.ml
- subst,metasenv,t1,t2,ugraph
- in
- begin
- match t1',t2' with
- C.Appl l1, C.Appl l2 ->
- let lr1 = List.rev l1 in
-=======
---------*)
let lr1 = List.rev l1 in
let lr2 = List.rev l2 in
let rec
"Can't unify %s with %s because they are not convertible"
(CicMetaSubst.ppterm subst t1)
(CicMetaSubst.ppterm subst t2))) *)
+ | (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 "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"))
| (_,_) ->
let b,ugraph1 =
R.are_convertible ~subst ~metasenv context t1 t2 ugraph
if b then
subst, metasenv, ugraph1
else
- raise (UnificationFailure "8")
+ raise (UnificationFailure "10")
(* (sprintf
"Can't unify %s with %s because they are not convertible"
(CicMetaSubst.ppterm subst t1)