1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
28 exception UnificationFailure of string;;
29 exception Uncertain of string;;
30 exception AssertFailure of string;;
32 let debug_print = fun _ -> ()
34 let type_of_aux' metasenv subst context term ugraph =
36 CicTypeChecker.type_of_aux' ~subst metasenv context term ugraph
38 CicTypeChecker.TypeCheckerFailure msg ->
41 "Kernel Type checking error:
42 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
43 (CicMetaSubst.ppterm subst term)
44 (CicMetaSubst.ppterm [] term)
45 (CicMetaSubst.ppcontext subst context)
46 (CicMetaSubst.ppmetasenv metasenv subst)
47 (CicMetaSubst.ppsubst subst) msg) in
48 raise (AssertFailure msg);;
51 List.exists (function Cic.Meta _ -> true | _ -> false) l
55 (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
56 let he'' = CicSubstitution.subst he' t in
60 beta_reduce (Cic.Appl(he''::tl'))
64 let snd (_,a,_) = a in
69 (CicSubstitution.subst_meta
70 l (snd (CicUtil.lookup_subst n subst)))
72 CicUtil.Subst_not_found _ -> t)
76 let rec deref subst t =
77 let snd (_,a,_) = a in
82 (CicSubstitution.subst_meta
83 l (snd (CicUtil.lookup_subst n subst)))
85 CicUtil.Subst_not_found _ -> t)
86 | Cic.Appl(Cic.Meta(n,l)::args) ->
87 (match deref subst (Cic.Meta(n,l)) with
88 | Cic.Lambda _ as t ->
89 deref subst (beta_reduce (Cic.Appl(t::args)))
90 | r -> Cic.Appl(r::args))
91 | Cic.Appl(((Cic.Lambda _) as t)::args) ->
92 deref subst (beta_reduce (Cic.Appl(t::args)))
97 let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
98 let module S = CicSubstitution in
100 let rec aux metasenv subst n context t' ugraph =
103 let subst,metasenv,ugraph1 =
104 fo_unif_subst test_equality_only subst context metasenv
105 (CicSubstitution.lift n arg) t' ugraph
108 subst,metasenv,C.Rel (1 + n),ugraph1
111 | UnificationFailure _ ->
113 | C.Rel m -> subst,metasenv,
114 (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
115 | C.Var (uri,exp_named_subst) ->
116 let subst,metasenv,exp_named_subst',ugraph1 =
117 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
119 subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
121 (* andrea: in general, beta_expand can create badly typed
122 terms. This happens quite seldom in practice, UNLESS we
123 iterate on the local context. For this reason, we renounce
124 to iterate and just lift *)
128 Some t -> Some (CicSubstitution.lift 1 t)
130 subst, metasenv, C.Meta (i,l), ugraph
132 | C.Implicit _ as t -> subst,metasenv,t,ugraph
134 let subst,metasenv,te',ugraph1 =
135 aux metasenv subst n context te ugraph in
136 let subst,metasenv,ty',ugraph2 =
137 aux metasenv subst n context ty ugraph1 in
138 (* TASSI: sure this is in serial? *)
139 subst,metasenv,(C.Cast (te', ty')),ugraph2
141 let subst,metasenv,s',ugraph1 =
142 aux metasenv subst n context s ugraph in
143 let subst,metasenv,t',ugraph2 =
144 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
147 (* TASSI: sure this is in serial? *)
148 subst,metasenv,(C.Prod (nn, s', t')),ugraph2
149 | C.Lambda (nn,s,t) ->
150 let subst,metasenv,s',ugraph1 =
151 aux metasenv subst n context s ugraph in
152 let subst,metasenv,t',ugraph2 =
153 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
155 (* TASSI: sure this is in serial? *)
156 subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
157 | C.LetIn (nn,s,t) ->
158 let subst,metasenv,s',ugraph1 =
159 aux metasenv subst n context s ugraph in
160 let subst,metasenv,t',ugraph2 =
161 aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t
164 (* TASSI: sure this is in serial? *)
165 subst,metasenv,(C.LetIn (nn, s', t')),ugraph2
167 let subst,metasenv,revl',ugraph1 =
169 (fun (subst,metasenv,appl,ugraph) t ->
170 let subst,metasenv,t',ugraph1 =
171 aux metasenv subst n context t ugraph in
172 subst,metasenv,(t'::appl),ugraph1
173 ) (subst,metasenv,[],ugraph) l
175 subst,metasenv,(C.Appl (List.rev revl')),ugraph1
176 | C.Const (uri,exp_named_subst) ->
177 let subst,metasenv,exp_named_subst',ugraph1 =
178 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
180 subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
181 | C.MutInd (uri,i,exp_named_subst) ->
182 let subst,metasenv,exp_named_subst',ugraph1 =
183 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
185 subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
186 | C.MutConstruct (uri,i,j,exp_named_subst) ->
187 let subst,metasenv,exp_named_subst',ugraph1 =
188 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
190 subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
191 | C.MutCase (sp,i,outt,t,pl) ->
192 let subst,metasenv,outt',ugraph1 =
193 aux metasenv subst n context outt ugraph in
194 let subst,metasenv,t',ugraph2 =
195 aux metasenv subst n context t ugraph1 in
196 let subst,metasenv,revpl',ugraph3 =
198 (fun (subst,metasenv,pl,ugraph) t ->
199 let subst,metasenv,t',ugraph1 =
200 aux metasenv subst n context t ugraph in
201 subst,metasenv,(t'::pl),ugraph1
202 ) (subst,metasenv,[],ugraph2) pl
204 subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
205 (* TASSI: not sure this is serial *)
207 (*CSC: not implemented
208 let tylen = List.length fl in
211 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
214 C.Fix (i, substitutedfl)
216 subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
218 (*CSC: not implemented
219 let tylen = List.length fl in
222 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
225 C.CoFix (i, substitutedfl)
228 subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
230 and aux_exp_named_subst metasenv subst n context ens ugraph =
232 (fun (uri,t) (subst,metasenv,l,ugraph) ->
233 let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
234 subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
236 let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
238 FreshNamesGenerator.mk_fresh_name ~subst
239 metasenv context (Cic.Name "Heta") ~typ:argty
241 let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
242 subst, metasenv, C.Lambda (fresh_name,argty,t'), ugraph2
245 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
246 let subst,metasenv,hd,ugraph =
248 (fun arg (subst,metasenv,t,ugraph) ->
249 let subst,metasenv,t,ugraph1 =
250 beta_expand test_equality_only
251 metasenv subst context t arg ugraph
253 subst,metasenv,t,ugraph1
254 ) args (subst,metasenv,t,ugraph)
256 subst,metasenv,hd,ugraph
259 (* NUOVA UNIFICAZIONE *)
260 (* A substitution is a (int * Cic.term) list that associates a
261 metavariable i with its body.
262 A metaenv is a (int * Cic.term) list that associate a metavariable
264 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
265 a new substitution which is _NOT_ unwinded. It must be unwinded before
268 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
269 let module C = Cic in
270 let module R = CicReduction in
271 let module S = CicSubstitution in
272 let t1 = deref subst t1 in
273 let t2 = deref subst t2 in
275 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
278 subst, metasenv, ugraph
281 | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
282 let _,subst,metasenv,ugraph1 =
285 (fun (j,subst,metasenv,ugraph) t1 t2 ->
288 | _,None -> j+1,subst,metasenv,ugraph
289 | Some t1', Some t2' ->
290 (* First possibility: restriction *)
291 (* Second possibility: unification *)
292 (* Third possibility: convertibility *)
295 ~subst ~metasenv context t1' t2' ugraph
298 j+1,subst,metasenv, ugraph1
301 let subst,metasenv,ugraph2 =
304 subst context metasenv t1' t2' ugraph
306 j+1,subst,metasenv,ugraph2
309 | UnificationFailure _ ->
310 debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j));
311 let metasenv, subst =
312 CicMetaSubst.restrict
313 subst [(n,j)] metasenv in
314 j+1,subst,metasenv,ugraph1)
315 ) (1,subst,metasenv,ugraph) ln lm
319 (UnificationFailure "1")
322 "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted."
323 (CicMetaSubst.ppterm subst t1)
324 (CicMetaSubst.ppterm subst t2))) *)
325 | Invalid_argument _ ->
327 (UnificationFailure "2"))
330 "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
331 (CicMetaSubst.ppterm subst t1)
332 (CicMetaSubst.ppterm subst t2)))) *)
333 in subst,metasenv,ugraph1
334 | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
335 fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
337 | (t, C.Meta (n,l)) ->
340 C.Meta (n,_), C.Meta (m,_) when n < m -> false
341 | _, C.Meta _ -> false
344 let lower = fun x y -> if swap then y else x in
345 let upper = fun x y -> if swap then x else y in
346 let fo_unif_subst_ordered
347 test_equality_only subst context metasenv m1 m2 ugraph =
348 fo_unif_subst test_equality_only subst context metasenv
349 (lower m1 m2) (upper m1 m2) ugraph
352 let subst,metasenv,ugraph1 =
353 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
356 type_of_aux' metasenv subst context t ugraph
360 subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
362 UnificationFailure msg
364 (* debug_print msg; *)raise (UnificationFailure msg)
366 debug_print "siamo allo huge hack";
367 (* TODO huge hack!!!!
368 * we keep on unifying/refining in the hope that
369 * the problem will be eventually solved.
370 * In the meantime we're breaking a big invariant:
371 * the terms that we are unifying are no longer well
372 * typed in the current context (in the worst case
373 * we could even diverge) *)
374 (subst, metasenv,ugraph)) in
375 let t',metasenv,subst =
377 CicMetaSubst.delift n subst context metasenv l t
379 (CicMetaSubst.MetaSubstFailure msg)->
380 raise (UnificationFailure msg)
381 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
385 C.Sort (C.Type u) when not test_equality_only ->
386 let u' = CicUniv.fresh () in
387 let s = C.Sort (C.Type u') in
389 CicUniv.add_ge (upper u u') (lower u u') ugraph1
394 (* Unifying the types may have already instantiated n. Let's check *)
396 let (_, oldt,_) = CicUtil.lookup_subst n subst in
397 let lifted_oldt = S.subst_meta l oldt in
398 fo_unif_subst_ordered
399 test_equality_only subst context metasenv t lifted_oldt ugraph2
401 CicUtil.Subst_not_found _ ->
402 let (_, context, ty) = CicUtil.lookup_meta n metasenv in
403 let subst = (n, (context, t'',ty)) :: subst in
405 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
406 subst, metasenv, ugraph2
408 | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
409 | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
410 if UriManager.eq uri1 uri2 then
411 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
412 exp_named_subst1 exp_named_subst2 ugraph
414 raise (UnificationFailure "3")
416 "Can't unify %s with %s due to different constants"
417 (CicMetaSubst.ppterm subst t1)
418 (CicMetaSubst.ppterm subst t2))) *)
419 | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
420 if UriManager.eq uri1 uri2 && i1 = i2 then
421 fo_unif_subst_exp_named_subst
423 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
425 raise (UnificationFailure "4")
427 "Can't unify %s with %s due to different inductive principles"
428 (CicMetaSubst.ppterm subst t1)
429 (CicMetaSubst.ppterm subst t2))) *)
430 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
431 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
432 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
433 fo_unif_subst_exp_named_subst
435 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
437 raise (UnificationFailure "5")
439 "Can't unify %s with %s due to different inductive constructors"
440 (CicMetaSubst.ppterm subst t1)
441 (CicMetaSubst.ppterm subst t2))) *)
442 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
443 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
444 subst context metasenv te t2 ugraph
445 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
446 subst context metasenv t1 te ugraph
447 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
448 let subst',metasenv',ugraph1 =
449 fo_unif_subst true subst context metasenv s1 s2 ugraph
451 fo_unif_subst test_equality_only
452 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
453 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
454 let subst',metasenv',ugraph1 =
455 fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
457 fo_unif_subst test_equality_only
458 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
459 | (C.LetIn (_,s1,t1), t2)
460 | (t2, C.LetIn (_,s1,t1)) ->
462 test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
463 | (C.Appl l1, C.Appl l2) ->
464 (* andrea: this case should be probably rewritten in the
467 | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
470 (fun (subst,metasenv,ugraph) t1 t2 ->
472 test_equality_only subst context metasenv t1 t2 ugraph)
473 (subst,metasenv,ugraph) l1 l2
474 with (Invalid_argument msg) ->
475 raise (UnificationFailure msg))
476 | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
477 (* we verify that none of the args is a Meta,
478 since beta expanding with respoect to a metavariable
482 let (_,t,_) = CicUtil.lookup_subst i subst in
483 let lifted = S.subst_meta l t in
484 let reduced = beta_reduce (Cic.Appl (lifted::args)) in
487 subst context metasenv reduced t2 ugraph
488 with CicUtil.Subst_not_found _ -> *)
489 let subst,metasenv,beta_expanded,ugraph1 =
491 test_equality_only metasenv subst context t2 args ugraph
493 fo_unif_subst test_equality_only subst context metasenv
494 (C.Meta (i,l)) beta_expanded ugraph1
495 | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
497 let (_,t,_) = CicUtil.lookup_subst i subst in
498 let lifted = S.subst_meta l t in
499 let reduced = beta_reduce (Cic.Appl (lifted::args)) in
502 subst context metasenv t1 reduced ugraph
503 with CicUtil.Subst_not_found _ -> *)
504 let subst,metasenv,beta_expanded,ugraph1 =
507 metasenv subst context t1 args ugraph
509 fo_unif_subst test_equality_only subst context metasenv
510 (C.Meta (i,l)) beta_expanded ugraph1
512 let lr1 = List.rev l1 in
513 let lr2 = List.rev l2 in
515 fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
518 | _,[] -> assert false
521 test_equality_only subst context metasenv h1 h2 ugraph
524 fo_unif_subst test_equality_only subst context metasenv
525 h (C.Appl (List.rev l)) ugraph
526 | ((h1::l1),(h2::l2)) ->
527 let subst', metasenv',ugraph1 =
530 subst context metasenv h1 h2 ugraph
533 test_equality_only subst' metasenv' (l1,l2) ugraph1
536 test_equality_only subst metasenv (lr1, lr2) ugraph)
537 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
538 let subst', metasenv',ugraph1 =
539 fo_unif_subst test_equality_only subst context metasenv outt1 outt2
541 let subst'',metasenv'',ugraph2 =
542 fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
546 (fun (subst,metasenv,ugraph) t1 t2 ->
548 test_equality_only subst context metasenv t1 t2 ugraph
549 ) (subst'',metasenv'',ugraph2) pl1 pl2
551 Invalid_argument _ ->
552 raise (UnificationFailure "6"))
554 "Error trying to unify %s with %s: the number of branches is not the same."
555 (CicMetaSubst.ppterm subst t1)
556 (CicMetaSubst.ppterm subst t2)))) *)
557 | (C.Rel _, _) | (_, C.Rel _) ->
559 subst, metasenv,ugraph
561 raise (UnificationFailure "6")
563 "Can't unify %s with %s because they are not convertible"
564 (CicMetaSubst.ppterm subst t1)
565 (CicMetaSubst.ppterm subst t2))) *)
566 | (C.Sort _ ,_) | (_, C.Sort _)
567 | (C.Const _, _) | (_, C.Const _)
568 | (C.MutInd _, _) | (_, C.MutInd _)
569 | (C.MutConstruct _, _) | (_, C.MutConstruct _)
570 | (C.Fix _, _) | (_, C.Fix _)
571 | (C.CoFix _, _) | (_, C.CoFix _) ->
573 subst, metasenv, ugraph
576 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
579 subst, metasenv, ugraph1
581 raise (* (UnificationFailure "7") *)
582 (UnificationFailure (sprintf
583 "Can't unify %s with %s because they are not convertible"
584 (CicMetaSubst.ppterm subst t1)
585 (CicMetaSubst.ppterm subst t2)))
586 | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
587 let subst,metasenv,beta_expanded,ugraph1 =
589 test_equality_only metasenv subst context t2 args ugraph
591 fo_unif_subst test_equality_only subst context metasenv
592 (C.Meta (i,l)) beta_expanded ugraph1
593 | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
594 let subst,metasenv,beta_expanded,ugraph1 =
596 test_equality_only metasenv subst context t1 args ugraph
598 fo_unif_subst test_equality_only subst context metasenv
599 beta_expanded (C.Meta (i,l)) ugraph1
601 let t2' = R.whd ~subst context t2 in
604 fo_unif_subst test_equality_only
605 subst context metasenv t1 t2' ugraph
606 | _ -> raise (UnificationFailure "8"))
608 let t1' = R.whd ~subst context t1 in
611 fo_unif_subst test_equality_only
612 subst context metasenv t1' t2 ugraph
613 | _ -> (* raise (UnificationFailure "9")) *)
615 (UnificationFailure (sprintf
616 "Can't unify %s with %s because they are not convertible"
617 (CicMetaSubst.ppterm subst t1)
618 (CicMetaSubst.ppterm subst t2))))
621 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
624 subst, metasenv, ugraph1
626 raise (UnificationFailure "10")
628 "Can't unify %s with %s because they are not convertible"
629 (CicMetaSubst.ppterm subst t1)
630 (CicMetaSubst.ppterm subst t2))) *)
632 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
633 exp_named_subst1 exp_named_subst2 ugraph
637 (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
639 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
640 ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
642 Invalid_argument _ ->
647 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
650 raise (UnificationFailure (sprintf
651 "Error trying to unify the two explicit named substitutions (local contexts) %s and %s: their lengths is different." (print_ens exp_named_subst1) (print_ens exp_named_subst2)))
653 (* A substitution is a (int * Cic.term) list that associates a *)
654 (* metavariable i with its body. *)
655 (* metasenv is of type Cic.metasenv *)
656 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
657 (* a new substitution which is already unwinded and ready to be applied and *)
658 (* a new metasenv in which some hypothesis in the contexts of the *)
659 (* metavariables may have been restricted. *)
660 let fo_unif metasenv context t1 t2 ugraph =
661 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
663 let fo_unif_subst subst context metasenv t1 t2 ugraph =
664 let enrich_msg msg = (* "bella roba" *)
665 sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nand substitution\n%s\nbecause %s"
666 (CicMetaSubst.ppterm subst t1)
668 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
670 with _ -> "MALFORMED")
671 (CicMetaSubst.ppterm subst t2)
673 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
675 with _ -> "MALFORMED")
676 (CicMetaSubst.ppcontext subst context)
677 (CicMetaSubst.ppmetasenv metasenv subst)
678 (CicMetaSubst.ppsubst subst) msg
681 fo_unif_subst false subst context metasenv t1 t2 ugraph
683 | AssertFailure msg -> raise (AssertFailure (enrich_msg msg))
684 | UnificationFailure msg -> raise (UnificationFailure (enrich_msg msg))