remove_refl p1
| _ -> Cic.Appl (List.map remove_refl args))
| Cic.Appl l -> Cic.Appl (List.map remove_refl l)
- | Cic.LetIn (name,bo,rest) ->
- Cic.LetIn (name,remove_refl bo,remove_refl rest)
+ | Cic.LetIn (name,bo,ty,rest) ->
+ Cic.LetIn (name,remove_refl bo,remove_refl ty,remove_refl rest)
| _ -> t
in
let rec canonical_trough_lambda context = function
and canonical context t =
match t with
- | Cic.LetIn(name,bo,rest) ->
+ | Cic.LetIn(name,bo,ty,rest) ->
let bo = canonical_trough_lambda context bo in
- let context' = (Some (name,Cic.Def (bo,None)))::context in
- Cic.LetIn(name,bo,canonical context' rest)
+ let ty = canonical_trough_lambda context ty in
+ let context' = (Some (name,Cic.Def (bo,ty)))::context in
+ Cic.LetIn(name,bo,ty,canonical context' rest)
| Cic.Appl (((Cic.Const(uri_sym,ens))::tl) as args)
when LibraryObjects.is_sym_eq_URI uri_sym ->
(match p_of_sym ens tl with
when LibraryObjects.is_sym_eq_URI uri_sym ->
let ty,l,r,p = open_sym ens tl in
mk_sym uri_sym ty l r (aux uri ty l r ctx_d ctx_ty p)
- | Cic.LetIn (name,body,rest) ->
- Cic.LetIn (name,look_ahead (aux uri) body, aux uri ty left right ctx_d ctx_ty rest)
+ | Cic.LetIn (name,body,bodyty,rest) ->
+ Cic.LetIn
+ (name,look_ahead (aux uri) body, bodyty,
+ aux uri ty left right ctx_d ctx_ty rest)
| Cic.Appl ((Cic.Const(uri_ind,ens))::tl)
when LibraryObjects.is_eq_ind_URI uri_ind ||
LibraryObjects.is_eq_ind_r_URI uri_ind ->
acc@[id,real_cic],n+1,h)
([],0,[]) lets
in
+ let lets =
+ List.map (fun (id,cic) -> id,cic,Cic.Implicit (Some `Type)) lets
+ in
let proof,se =
let rec aux se current_proof = function
| [] -> current_proof,se
let n,proof =
let initial = proof in
List.fold_right
- (fun (id,cic) (n,p) ->
+ (fun (id,cic,ty) (n,p) ->
n-1,
Cic.LetIn (
Cic.Name ("H"^string_of_int id),
- cic, p))
+ cic,
+ ty,
+ p))
lets (letsno-1,initial)
in
canonical
aux_ens table ens1 ens2
| C.Cast (s1, t1), C.Cast (s2, t2)
| C.Prod (_, s1, t1), C.Prod (_, s2, t2)
- | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
- | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
+ | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2) ->
+ let table = aux table s1 s2 in
+ aux table t1 t2
+ | C.LetIn (_, s1, ty1, t1), C.LetIn (_, s2, ty2, t2) ->
let table = aux table s1 s2 in
+ let table = aux table ty1 ty2 in
aux table t1 t2
| C.Appl l1, C.Appl l2 -> (
try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
| _ -> assert false
in
let rec skip_letin ctx = function
- | Cic.LetIn (n,b,t) ->
+ | Cic.LetIn (n,b,_,t) ->
pp_proofterm (Some (rename "Lemma " n)) b ctx::
skip_letin ((Some n)::ctx) t
| t ->