diff options
Diffstat (limited to 'tactics/rewrite.ml')
| -rw-r--r-- | tactics/rewrite.ml | 47 |
1 files changed, 28 insertions, 19 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index a3914da1..ac8b4923 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -283,7 +283,7 @@ end) = struct (app_poly env evd arrow [| a; b |]), unfold_impl (* (evd, mkProd (Anonymous, a, b)), (fun x -> x) *) else if bp then (* Dummy forall *) - (app_poly env evd coq_all [| a; mkLambda (Anonymous, a, b) |]), unfold_forall + (app_poly env evd coq_all [| a; mkLambda (Anonymous, a, lift 1 b) |]), unfold_forall else (* None in Prop, use arrow *) (app_poly env evd arrow [| a; b |]), unfold_impl @@ -629,11 +629,9 @@ let solve_remaining_by env sigma holes by = | None -> sigma (** Evar should not be defined, but just in case *) | Some evi -> - let ctx = Evd.evar_universe_context sigma in let env = Environ.reset_with_named_context evi.evar_hyps env in let ty = evi.evar_concl in - let c, _, ctx = Pfedit.build_by_tactic env ctx ty solve_tac in - let sigma = Evd.set_universe_context sigma ctx in + let c, sigma = Pfedit.refine_by_tactic env sigma ty solve_tac in Evd.define evk c sigma in List.fold_left solve sigma indep @@ -1446,7 +1444,14 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul let newt = Evarutil.nf_evar evars' res.rew_to in let evars = (* Keep only original evars (potentially instantiated) and goal evars, the rest has been defined and substituted already. *) - Evar.Set.fold (fun ev acc -> Evd.remove acc ev) cstrs evars' + Evar.Set.fold + (fun ev acc -> + if not (Evd.is_defined acc ev) then + errorlabstrm "rewrite" + (str "Unsolved constraint remaining: " ++ spc () ++ + Evd.pr_evar_info (Evd.find acc ev)) + else Evd.remove acc ev) + cstrs evars' in let res = match res.rew_prf with | RewCast c -> None @@ -1466,28 +1471,32 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul in Some proof in Some (Some (evars, res, newt)) +(** Insert a declaration after the last declaration it depends on *) +let rec insert_dependent env decl accu hyps = match hyps with +| [] -> List.rev_append accu [decl] +| (id, _, _ as ndecl) :: rem -> + if occur_var_in_decl env id decl then + List.rev_append accu (decl :: hyps) + else + insert_dependent env decl (ndecl :: accu) rem + let assert_replacing id newt tac = let prf = Proofview.Goal.nf_enter begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in - let nc' = - Environ.fold_named_context - (fun _ (n, b, t as decl) nc' -> - if Id.equal n id then (n, b, newt) :: nc' - else decl :: nc') - env ~init:[] + let ctx = Environ.named_context env in + let after, before = List.split_when (fun (n, b, t) -> Id.equal n id) ctx in + let nc = match before with + | [] -> assert false + | (id, b, _) :: rem -> insert_dependent env (id, b, newt) [] after @ rem in + let env' = Environ.reset_with_named_context (val_of_named_context nc) env in Proofview.Refine.refine ~unsafe:false begin fun sigma -> - let env' = Environ.reset_with_named_context (val_of_named_context nc') env in let sigma, ev = Evarutil.new_evar env' sigma concl in let sigma, ev' = Evarutil.new_evar env sigma newt in - let fold _ (n, b, t) inst = - if Id.equal n id then ev' :: inst - else mkVar n :: inst - in - let inst = fold_named_context fold env ~init:[] in - let (e, args) = destEvar ev in - sigma, mkEvar (e, Array.of_list inst) + let map (n, _, _) = if Id.equal n id then ev' else mkVar n in + let (e, _) = destEvar ev in + sigma, mkEvar (e, Array.map_of_list map nc) end end in Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac) |