diff options
Diffstat (limited to 'tactics/rewrite.ml')
-rw-r--r-- | tactics/rewrite.ml | 62 |
1 files changed, 0 insertions, 62 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 22dc93d1a..a10b62162 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1818,65 +1818,3 @@ let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity let _ = Hook.set Tactics.setoid_symmetry setoid_symmetry let _ = Hook.set Tactics.setoid_symmetry_in setoid_symmetry_in let _ = Hook.set Tactics.setoid_transitivity setoid_transitivity - - -let implify id gl = - let (_, b, ctype) = pf_get_hyp gl id in - let binders,concl = decompose_prod_assum ctype in - let ctype' = - match binders with - | (_, None, ty as hd) :: tl when noccurn 1 concl -> - let env = Environ.push_rel_context tl (pf_env gl) in - let sigma = project gl in - let tyhd = Typing.type_of env sigma ty - and tyconcl = Typing.type_of (Environ.push_rel hd env) sigma concl in - let app, unfold = arrow_morphism tyhd (subst1 mkProp tyconcl) ty (subst1 mkProp concl) in - it_mkProd_or_LetIn app tl - | _ -> ctype - in convert_hyp_no_check (id, b, ctype') gl - -let rec fold_matches eff env sigma c = - map_constr_with_full_binders Environ.push_rel - (fun env c -> - match kind_of_term c with - | Case _ -> - let cst, env, c',eff' = fold_match ~force:true env sigma c in - eff := Declareops.union_side_effects eff' !eff; - fold_matches eff env sigma c' - | _ -> fold_matches eff env sigma c) - env c - -let fold_matches_tac c gl = - let eff = ref Declareops.no_seff in - let c' = fold_matches eff (pf_env gl) (project gl) c in - tclTHEN (Tactics.emit_side_effects !eff) - (change (Some (snd (pattern_of_constr (project gl) c))) c' onConcl) gl - -let myapply id l gl = - let gr = id in - let _, impls = List.hd (Impargs.implicits_of_global gr) in - let ty = Global.type_of_global gr in - let env = pf_env gl in - let evars = ref (project gl) in - let app = - let rec aux ty impls args args' = - match impls, kind_of_term ty with - | Some (_, _, (_, _)) :: impls, Prod (n, t, t') -> - let arg = Evarutil.e_new_evar evars env t in - aux (subst1 arg t') impls args (arg :: args') - | None :: impls, Prod (n, t, t') -> - (match args with - | [] -> - if dependent (mkRel 1) t' then - let arg = Evarutil.e_new_evar evars env t in - aux (subst1 arg t') impls args (arg :: args') - else - let arg = Evarutil.mk_new_meta () in - evars := meta_declare (destMeta arg) t !evars; - aux (subst1 arg t') impls args (arg :: args') - | arg :: args -> - aux (subst1 arg t') impls args (arg :: args')) - | _, _ -> mkApp (constr_of_global gr, Array.of_list (List.rev args')) - in aux ty impls l [] - in - tclTHEN (Refiner.tclEVARS !evars) (apply app) gl |