| C.Meta (i, _), C.Meta (j, _) when i > j ->
unif subst menv t s
| C.Meta _, t when occurs_check subst s t ->
| C.Meta (i, _), C.Meta (j, _) when i > j ->
unif subst menv t s
| C.Meta _, t when occurs_check subst s t ->
assert false
)
| _, C.Meta _ -> unif subst menv t s
| C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
assert false
)
| _, C.Meta _ -> unif subst menv t s
| C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
| C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
try
List.fold_left2
(fun (subst', menv) s t -> unif subst' menv s t)
(subst, menv) tls tlt
with Invalid_argument _ ->
| C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
try
List.fold_left2
(fun (subst', menv) s t -> unif subst' menv s t)
(subst, menv) tls tlt
with Invalid_argument _ ->
(* Printf.printf "| unification %s %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); *)
let subst, menv, ug =
if not (is_simple_term t1) || not (is_simple_term t2) then (
(* Printf.printf "| unification %s %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); *)
let subst, menv, ug =
if not (is_simple_term t1) || not (is_simple_term t2) then (
CicUnification.fo_unif metasenv context t1 t2 ugraph
) else
unification_simple metasenv context t1 t2 ugraph
CicUnification.fo_unif metasenv context t1 t2 ugraph
) else
unification_simple metasenv context t1 t2 ugraph
match head with
| C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
when (UriManager.eq uri eq_uri) && (ok_types ty newmetas) ->
match head with
| C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
when (UriManager.eq uri eq_uri) && (ok_types ty newmetas) ->
let o = !Utils.compare_terms t1 t2 in
let w = compute_equality_weight ty t1 t2 in
let proof = BasicProof p in
let o = !Utils.compare_terms t1 t2 in
let w = compute_equality_weight ty t1 t2 in
let proof = BasicProof p in
match head with
| C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
when (iseq uri) && (ok_types ty newmetas) ->
match head with
| C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
when (iseq uri) && (ok_types ty newmetas) ->
let o = !Utils.compare_terms t1 t2 in
let w = compute_equality_weight ty t1 t2 in
let proof = BasicProof p in
let o = !Utils.compare_terms t1 t2 in
let w = compute_equality_weight ty t1 t2 in
let proof = BasicProof p in