From 625a129d5e9b200399a147111f191abe84282aa4 Mon Sep 17 00:00:00 2001 From: msozeau Date: Fri, 6 Nov 2009 03:01:57 +0000 Subject: Misc fixes. - Correct backtracking function of coqdoc to handle the _p fields of lexers - Try a better typesetting of [[ ]] inline code considering it as blocks and not purely inline code like [ ] escapings. - Rework latex macros for better factorization and support external references in pdf output. - Better criterion for generalization of variables in dependent elimination tactic and better error message in [specialize_hypothesis]. - In autounfold, don't put the core unfolds by default. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12474 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/tactics.ml | 30 +++++++++++++++++++++++++++--- 1 file changed, 27 insertions(+), 3 deletions(-) (limited to 'tactics/tactics.ml') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index a740d7bb2..b9d2d9cfe 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2160,7 +2160,7 @@ let lift_together l = lift_togethern 0 l let lift_list l = List.map (lift 1) l -let ids_of_constr vars c = +let ids_of_constr ?(all=false) vars c = let rec aux vars c = match kind_of_term c with | Var id -> Idset.add id vars @@ -2169,7 +2169,8 @@ let ids_of_constr vars c = | Construct (ind,_) | Ind ind -> let (mib,mip) = Global.lookup_inductive ind in - array_fold_left_from mib.Declarations.mind_nparams + array_fold_left_from + (if all then 0 else mib.Declarations.mind_nparams) aux vars args | _ -> fold_constr aux vars c) | _ -> fold_constr aux vars c @@ -2248,6 +2249,23 @@ let hyps_of_vars env sign nogen hyps = sign in lh +exception Seen + +let linear vars args = + let seen = ref vars in + try + Array.iter (fun i -> + let rels = ids_of_constr ~all:true Idset.empty i in + let seen' = + Idset.fold (fun id acc -> + if Idset.mem id acc then raise Seen + else Idset.add id acc) + rels !seen + in seen := seen') + args; + true + with Seen -> false + let abstract_args gl generalize_vars dep id = let c = pf_get_hyp_typ gl id in let sigma = project gl in @@ -2299,7 +2317,8 @@ let abstract_args gl generalize_vars dep id = in let f', args' = decompose_indapp f args in let dogen, f', args' = - if not (array_distinct args) then true, f', args' + let parvars = ids_of_constr ~all:true Idset.empty f' in + if not (linear parvars args') then true, f, args else match array_find_i (fun i x -> not (isVar x)) args' with | None -> false, f', args' @@ -2390,6 +2409,11 @@ let specialize_hypothesis id gl = else tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) gl +let specialize_hypothesis id gl = + if occur_id [] id (pf_concl gl) then + tclFAIL 0 (str "Specialization not allowed on dependent hypotheses") gl + else specialize_hypothesis id gl + let dependent_pattern c gl = let cty = pf_type_of gl c in let deps = -- cgit v1.2.3