-
-(*
- let sym_eq = Cic.Const(uri_sym,ens) in
- let eq_f = Cic.Const(uri_feq,[]) in
- let b = Cic.MutConstruct (UriManager.uri_of_string
- "cic:/matita/datatypes/bool/bool.ind",0,1,[])
- in
- let u = ty1 in
- let ctx = f in
- let n = build_nat (count_args p) in
- let h = head_of_apply p in
- let predl = lambdaof true context (tyof context menv h) in
- let predr = lambdaof false context (tyof context menv h) in
- let args = tail_of_apply p in
- let appl =
- Cic.Appl
- ([Cic.Const(UriManager.uri_of_string
- "cic:/matita/paramodulation/rewrite.con",[]);
- eq; sym_eq; eq_f; b; u; ctx; n; predl; predr; h] @
- args)
- in
- appl
-*)
-(*
- | Cic.Appl (((Cic.Const(uri_ind,ens)) as he)::tl)
- when LibraryObjects.is_eq_ind_URI uri_ind ||
- LibraryObjects.is_eq_ind_r_URI uri_ind ->
- let ty, what, pred, p1, other, p2 =
- match tl with
- | [ty;what;pred;p1;other;p2] -> ty, what, pred, p1, other, p2
- | _ -> assert false
- in
- let pred,l,r =
- match pred with
- | Cic.Lambda (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;l;r])
- when LibraryObjects.is_eq_URI uri ->
- Cic.Lambda
- (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;r;l]),l,r
- | _ ->
- prerr_endline (CicPp.ppterm pred);
- assert false
- in
- let l = CicSubstitution.subst what l in
- let r = CicSubstitution.subst what r in
- Cic.Appl
- [he;ty;what;pred;
- canonical (mk_sym uri_sym ty l r p1);other;canonical p2]
-*)