collect_context ctx (howmany - 1) do_whd t
in
(context',ty,C.Lambda(n',s,bo))
- | C.LetIn (n,s,t) ->
+ | C.LetIn (n,s,sty,t) ->
let (context',ty,bo) =
- collect_context ((Some (n,(C.Def (s,None))))::context) (howmany - 1) do_whd t
+ collect_context ((Some (n,(C.Def (s,sty))))::context) (howmany - 1) do_whd t
in
- (context',ty,C.LetIn(n,s,bo))
+ (context',ty,C.LetIn(n,s,sty,bo))
| _ as t ->
if howmany <= 0 then
let irl =
| C.Cast (te,ty) -> C.Cast (aux n te, aux n ty)
| C.Prod (nn,s,t) -> C.Prod (nn, aux n s, aux (n+1) t)
| C.Lambda (nn,s,t) -> C.Lambda (nn, aux n s, aux (n+1) t)
- | C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t)
+ | C.LetIn (nn,s,ty,t) -> C.LetIn (nn, aux n s, aux n ty, aux (n+1) t)
| C.Appl l -> C.Appl (List.map (aux n) l)
| C.Const (uri,exp_named_subst) ->
let exp_named_subst' = aux_exp_named_subst n exp_named_subst in
match entry with
Some (n,Cic.Decl s) ->
Some (n,Cic.Decl (subst_in canonical_context' s))
- | Some (n,Cic.Def (s,None)) ->
- Some (n,Cic.Def ((subst_in canonical_context' s),None))
| None -> None
- | Some (n,Cic.Def (bo,Some ty)) ->
+ | Some (n,Cic.Def (bo,ty)) ->
Some
(n,
Cic.Def
(subst_in canonical_context' bo,
- Some (subst_in canonical_context' ty)))
+ subst_in canonical_context' ty))
in
entry'::canonical_context'
) canonical_context []
CicMkImplicit.identity_relocation_list_for_metavariable context
in
let newmeta1ty = CicSubstitution.lift 1 ty in
-(* This is the pre-letin implementation
- let bo' =
- C.Appl
- [C.Lambda (fresh_name,term,C.Meta (newmeta1,irl1)) ;
- C.Meta (newmeta2,irl2)]
- in
-*)
let bo' =
- Cic.LetIn (fresh_name, C.Meta (newmeta2,irl2), C.Meta (newmeta1,irl1))
+ Cic.LetIn (fresh_name, C.Meta (newmeta2,irl2), term, C.Meta (newmeta1,irl1))
in
let (newproof, _) =
ProofEngineHelpers.subst_meta_in_proof proof metano bo'
let fresh_name =
mk_fresh_name_callback metasenv context (Cic.Name "Hletin") ~typ:term in
let context_for_newmeta =
- (Some (fresh_name,C.Def (term,Some tty)))::context in
+ (Some (fresh_name,C.Def (term,tty)))::context in
let irl =
CicMkImplicit.identity_relocation_list_for_metavariable
context_for_newmeta
in
let newmetaty = CicSubstitution.lift 1 ty in
- let bo' = C.LetIn (fresh_name,term,C.Meta (newmeta,irl)) in
+ let bo' = C.LetIn (fresh_name,term,tty,C.Meta (newmeta,irl)) in
let (newproof, _) =
ProofEngineHelpers.subst_meta_in_proof
proof metano bo'[newmeta,context_for_newmeta,newmetaty]
| C.Lambda (_, s, t) ->
let s, t = gen_term k s, gen_term (succ k) t in
if is_meta [s; t] then meta else C.Lambda (anon, s, t)
- | C.LetIn (_, s, t) ->
- let s, t = gen_term k s, gen_term (succ k) t in
- if is_meta [s; t] then meta else C.LetIn (anon, s, t)
+ | C.LetIn (_, s, ty, t) ->
+ let s,ty,t = gen_term k s, gen_term k ty, gen_term (succ k) t in
+ if is_meta [s; t] then meta else C.LetIn (anon, s, ty, t)
| C.Fix (i, fl) -> C.Fix (i, List.map (gen_fix (List.length fl) k) fl)
| C.CoFix (i, fl) -> C.CoFix (i, List.map (gen_cofix (List.length fl) k) fl)
in
[ReductionTactics.simpl_tac
~pattern:(ProofEngineTypes.conclusion_pattern None)])
;;
-
-(* FG: insetrts a "hole" in the context (derived from letin_tac) *)
-
-let letout_tac =
- let mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[] in
- let term = C.Sort C.Set in
- let letout_tac (proof, goal) =
- let curi, metasenv, _subst, pbo, pty, attrs = proof in
- let metano, context, ty = CicUtil.lookup_meta goal metasenv in
- let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
- let fresh_name = mk_fresh_name_callback metasenv context (Cic.Name "hole") ~typ:term in
- let context_for_newmeta = None :: context in
- let irl = CicMkImplicit.identity_relocation_list_for_metavariable context_for_newmeta in
- let newmetaty = CicSubstitution.lift 1 ty in
- let bo' = C.LetIn (fresh_name, term, C.Meta (newmeta,irl)) in
- let newproof, _ = ProofEngineHelpers.subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty] in
- newproof, [newmeta]
- in
- PET.mk_tactic letout_tac