let module PEH = ProofEngineHelpers in
let module PT = PrimitiveTactics in
assert (wanted = None); (* this should be checked syntactically *)
let module PEH = ProofEngineHelpers in
let module PT = PrimitiveTactics in
assert (wanted = None); (* this should be checked syntactically *)
let proof,goal = status in
let curi, metasenv, pbo, pty = proof in
let (metano,context,gty) as conjecture = CicUtil.lookup_meta goal metasenv in
let proof,goal = status in
let curi, metasenv, pbo, pty = proof in
let (metano,context,gty) as conjecture = CicUtil.lookup_meta goal metasenv in
| _ ->
let arg,dir2,tac,concl_pat,gty =
match hyps_pat with
| _ ->
let arg,dir2,tac,concl_pat,gty =
match hyps_pat with
- [] -> None,true,PT.exact_tac,concl_pat,gty
+ [] -> None,true,(fun ~term _ -> PT.exact_tac term),concl_pat,gty
let rec find_hyp n =
function
[] -> assert false
| Some (Cic.Name s,Cic.Decl ty)::_ when name = s ->
Cic.Rel n, CicSubstitution.lift n ty
let rec find_hyp n =
function
[] -> assert false
| Some (Cic.Name s,Cic.Decl ty)::_ when name = s ->
Cic.Rel n, CicSubstitution.lift n ty
| _::tl -> find_hyp (n+1) tl
in
let arg,gty = find_hyp 1 context in
| _::tl -> find_hyp (n+1) tl
in
let arg,gty = find_hyp 1 context in
Tacticals.seq
~tactics:
[ProofEngineStructuralRules.rename name dummy;
PT.letin_tac
~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name name) term;
ProofEngineStructuralRules.clearbody name;
Tacticals.seq
~tactics:
[ProofEngineStructuralRules.rename name dummy;
PT.letin_tac
~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name name) term;
ProofEngineStructuralRules.clearbody name;
- (None,[name,Cic.Implicit (Some `Hole)],Cic.Implicit None);
+ (None,[name,Cic.Implicit (Some `Hole)],Cic.Implicit None)
+ (ProofEngineTypes.const_lazy_term typ);
let pred = C.Lambda (fresh_name, ty, abstr_gty) in
(* The argument is either a meta if we are rewriting in the conclusion
or the hypothesis if we are rewriting in an hypothesis *)
let pred = C.Lambda (fresh_name, ty, abstr_gty) in
(* The argument is either a meta if we are rewriting in the conclusion
or the hypothesis if we are rewriting in an hypothesis *)
match arg with
None ->
let gty' = CicSubstitution.subst t2 abstr_gty in
let irl =
CicMkImplicit.identity_relocation_list_for_metavariable context in
let metasenv' = (fresh_meta,context,gty')::metasenv' in
match arg with
None ->
let gty' = CicSubstitution.subst t2 abstr_gty in
let irl =
CicMkImplicit.identity_relocation_list_for_metavariable context in
let metasenv' = (fresh_meta,context,gty')::metasenv' in
- metasenv', C.Meta (fresh_meta,irl)
+ metasenv', C.Meta (fresh_meta,irl), Cic.Rel (-1) (* dummy term, never used *)
- (tac ~term:exact_proof) ((curi,metasenv',pbo,pty),goal)
+ (tac ~term:exact_proof newtyp) ((curi,metasenv',pbo,pty),goal)