diff options
| -rw-r--r-- | contrib/funind/functional_principles_proofs.ml | 16 | ||||
| -rw-r--r-- | contrib/recdef/recdef.ml4 | 24 |
2 files changed, 17 insertions, 23 deletions
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index 06f8673d0..2dbf1d107 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -177,18 +177,6 @@ let isAppConstruct t = let nf_betaiotazeta = Reductionops.local_strong Reductionops.whd_betaiotazeta -let rec subst_rel_map sub t = - match kind_of_term t with - | Rel k -> - begin - try - Intmap.find (k+1) sub - with Not_found -> - t - end - | _ -> map_constr (subst_rel_map sub) t - - let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type = let nochange msg = begin @@ -237,11 +225,11 @@ let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type = (* Ugly hack to prevent Map.fold order change between ocaml-3.08.3 and ocaml-3.08.4 Can be safely replaced by the next comment for Ocaml >= 3.08.4 *) - let sub' = Intmap.fold (fun i t acc = (i,t)::acc) sub [] in + let sub' = Intmap.fold (fun i t acc -> (i,t)::acc) sub [] in let sub'' = List.sort (fun (x,_) (y,_) -> Pervasives.compare x y) sub' in List.fold_left (fun end_of_type (i,t) -> lift 1 (substnl [t] (i-1) end_of_type)) end_of_type_with_pop - sub + sub'' in (* let new_end_of_type = *) (* Intmap.fold *) diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index 21ee8cf6b..d91806074 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -49,6 +49,16 @@ open Genarg let qed () = Command.save_named true let defined () = Command.save_named false +let pf_get_new_ids idl g = + let ids = pf_ids_of_hyps g in + List.fold_right + (fun id acc -> next_global_ident_away false id (acc@ids)::acc) + idl + [] + +let pf_get_new_id id g = + List.hd (pf_get_new_ids [id] g) + let h_intros l = tclMAP h_intro l @@ -242,7 +252,6 @@ let mkCaseEq a : tactic = let rec mk_intros_and_continue (extra_eqn:bool) cont_function (eqs:constr list) (expr:constr) g = - let ids = pf_ids_of_hyps g in match kind_of_term expr with | Lambda (n, _, b) -> let n1 = @@ -302,6 +311,7 @@ let list_rewrite (rev:bool) (eqs: constr list) = let base_leaf_terminate (func:global_reference) eqs expr = (* let _ = msgnl (str "entering base_leaf") in *) (fun g -> + let [k';h] = pf_get_new_ids [k_id;h_id] g in tclTHENLIST [observe_tac "first split" (split (ImplicitBindings [expr])); observe_tac "second split" (split (ImplicitBindings [delayed_force coq_O])); @@ -355,15 +365,11 @@ let rec list_cond_rewrite k def pmax cond_eqs le_proofs = [] -> tclIDTAC | eq::eqs -> (fun g -> - let eq_t = pf_type_of g (mkVar eq) in - let (na,_,eq_t') = destProd eq_t in - let _,_,eq_t'' = destProd eq_t' in - let na',_,_ = destProd eq_t'' in tclTHENS (general_rewrite_bindings false (mkVar eq, - ExplicitBindings[dummy_loc, NamedHyp k, mkVar k; - dummy_loc, NamedHyp def, mkVar def])) + ExplicitBindings[dummy_loc, NamedHyp k_id, mkVar k; + dummy_loc, NamedHyp def_id, mkVar def])) [list_cond_rewrite k def pmax eqs le_proofs; make_lt_proof pmax le_proofs] g ) @@ -968,9 +974,9 @@ let rec introduce_all_values_eq cont_tac functional termine (general_rewrite_bindings false (mkVar heq, ExplicitBindings - [dummy_loc, NamedHyp (next_global_ident_away true k_id ids), + [dummy_loc, NamedHyp k_id, f_S(mkVar pmax'); - dummy_loc, NamedHyp (next_global_ident_away true def_id ids), f])) + dummy_loc, NamedHyp def_id, f])) [tclIDTAC; tclTHENLIST [apply (delayed_force le_lt_n_Sm); |