diff options
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 73 |
1 files changed, 8 insertions, 65 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b99a45103..12aef852d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -15,7 +15,6 @@ open CErrors open Util open Names open Nameops -open Term open Constr open Termops open Environ @@ -89,18 +88,6 @@ let _ = optread = (fun () -> !universal_lemma_under_conjunctions) ; optwrite = (fun b -> universal_lemma_under_conjunctions := b) } -(* Shrinking of abstract proofs. *) - -let shrink_abstract = ref true - -let _ = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "shrinking of abstracted proofs"; - optkey = ["Shrink"; "Abstract"]; - optread = (fun () -> !shrink_abstract) ; - optwrite = (fun b -> shrink_abstract := b) } - (* The following boolean governs what "intros []" do on examples such as "forall x:nat*nat, x=x"; if true, it behaves as "intros [? ?]"; if false, it behaves as "intro H; case H; clear H" for fresh H. @@ -400,12 +387,11 @@ let find_name mayrepl decl naming gl = match naming with new_fresh_id idl (default_id env sigma decl) gl | NamingBasedOn (id,idl) -> new_fresh_id idl id gl | NamingMustBe (loc,id) -> - (* When name is given, we allow to hide a global name *) - let ids_of_hyps = Tacmach.New.pf_ids_set_of_hyps gl in - let id' = next_ident_away id ids_of_hyps in - if not mayrepl && not (Id.equal id' id) then - user_err ?loc (Id.print id ++ str" is already used."); - id + (* When name is given, we allow to hide a global name *) + let ids_of_hyps = Tacmach.New.pf_ids_set_of_hyps gl in + if not mayrepl && Id.Set.mem id ids_of_hyps then + user_err ?loc (Id.print id ++ str" is already used."); + id (**************************************************************) (* Computing position of hypotheses for replacing *) @@ -1339,46 +1325,6 @@ let index_of_ind_arg sigma t = | None -> error "Could not find inductive argument of elimination scheme." in aux None 0 t -let enforce_prop_bound_names rename tac = - let open Context.Rel.Declaration in - match rename with - | Some (isrec,nn) when Namegen.use_h_based_elimination_names () -> - (* Rename dependent arguments in Prop with name "H" *) - (* so as to avoid having hypothesis such as "t:True", "n:~A" when calling *) - (* elim or induction with schemes built by Indrec.build_induction_scheme *) - let rec aux env sigma i t = - if i = 0 then t else match EConstr.kind sigma t with - | Prod (Name _ as na,t,t') -> - let very_standard = true in - let na = - if Retyping.get_sort_family_of env sigma t = InProp then - (* "very_standard" says that we should have "H" names only, but - this would break compatibility even more... *) - let s = match Namegen.head_name sigma t with - | Some id when not very_standard -> Id.to_string id - | _ -> "" in - Name (add_suffix Namegen.default_prop_ident s) - else - na in - mkProd (na,t,aux (push_rel (LocalAssum (na,t)) env) sigma (i-1) t') - | Prod (Anonymous,t,t') -> - mkProd (Anonymous,t,aux (push_rel (LocalAssum (Anonymous,t)) env) sigma (i-1) t') - | LetIn (na,c,t,t') -> - mkLetIn (na,c,t,aux (push_rel (LocalDef (na,c,t)) env) sigma (i-1) t') - | _ -> assert false in - let rename_branch i = - Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let t = Proofview.Goal.concl gl in - change_concl (aux env sigma i t) - end in - (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn) - tac - (Array.map rename_branch nn) - | _ -> - tac - let rec contract_letin_in_lam_header sigma c = match EConstr.kind sigma c with | Lambda (x,t,c) -> mkLambda (x,t,contract_letin_in_lam_header sigma c) @@ -1399,7 +1345,7 @@ let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags (str "The type of elimination clause is not well-formed.")) in let elimclause' = clenv_fchain ~flags indmv elimclause indclause in - enforce_prop_bound_names rename (Clenvtac.res_pf elimclause' ~with_evars ~with_classes ~flags) + Clenvtac.res_pf elimclause' ~with_evars ~with_classes ~flags end (* @@ -4221,7 +4167,7 @@ let induction_tac with_evars params indvars elim = let elimclause' = recolle_clenv i params indvars elimclause gl in (* one last resolution (useless?) *) let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in - enforce_prop_bound_names rename (Clenvtac.clenv_refine with_evars resolved) + Clenvtac.clenv_refine with_evars resolved end (* Apply induction "in place" taking into account dependent @@ -4986,10 +4932,7 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = let (_, info) = CErrors.push src in iraise (e, info) in - let const, args = - if !shrink_abstract then shrink_entry sign const - else (const, List.rev (Context.Named.to_instance Constr.mkVar sign)) - in + let const, args = shrink_entry sign const in let args = List.map EConstr.of_constr args in let cd = Entries.DefinitionEntry { const with Entries.const_entry_opaque = opaque } in let decl = (cd, if opaque then IsProof Lemma else IsDefinition Definition) in |