diff options
| author | letouzey | 2011-02-22 22:12:53 +0000 |
|---|---|---|
| committer | letouzey | 2011-02-22 22:12:53 +0000 |
| commit | bd6fc1fca8a907b950893a9af81ed1a79903c887 (patch) | |
| tree | 06c979e71674da71afb98d0cb5c1411725004094 | |
| parent | 4a2bd45d6b3c2adc90ac547f5afc0ebdd51c3293 (diff) | |
Try to fix the behavior of clenv_missing used when declaring hints
Before this patch, hints such as "Hint Resolve -> a" in success/Hints.v
were erroneously considered "eauto-only". We try to clarify the big
boolean expression via "if", and for the moment we remove
the detection of "nonlinearity" via duplicated_metas : on the example,
some nonlinearity was found for strange reason (beta expansion ?), and
after some discussion with Hugo, it is unclear whether this nonlinearity
stuff is useful at all. The next coqbench might provide some answer
to this question, we'll see
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13850 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | proofs/clenv.ml | 17 | ||||
| -rw-r--r-- | test-suite/success/Hints.v | 2 |
2 files changed, 4 insertions, 15 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index e00e278cd0..8c4faa11cf 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -245,28 +245,19 @@ let dependent_closure clenv mvs = mvs acc in aux mvs mvs -let duplicated_metas c = - let rec collrec (one,more as acc) c = - match kind_of_term c with - | Meta mv -> if List.mem mv one then (one,mv::more) else (mv::one,more) - | _ -> fold_constr collrec acc c - in - snd (collrec ([],[]) c) - let clenv_dependent_gen hyps_only ?(iter=true) clenv = let all_undefined = undefined_metas clenv.evd in let deps_in_concl = (mk_freelisted (clenv_type clenv)).freemetas in let deps_in_hyps = dependent_in_type_of_metas clenv all_undefined in - let non_linear = duplicated_metas (clenv_value clenv) in let deps_in_concl = if hyps_only && iter then dependent_closure clenv deps_in_concl else deps_in_concl in List.filter (fun mv -> - Metaset.mem mv deps_in_hyps && - not (hyps_only && Metaset.mem mv deps_in_concl) - || not hyps_only && Metaset.mem mv deps_in_concl - || List.mem mv non_linear) + if hyps_only then + Metaset.mem mv deps_in_hyps && not (Metaset.mem mv deps_in_concl) + else + Metaset.mem mv deps_in_hyps || Metaset.mem mv deps_in_concl) all_undefined let clenv_missing ce = clenv_dependent_gen true ce diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index 6bbb0ff171..a93f890006 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -51,8 +51,6 @@ Axiom a : forall n, n=0 <-> n<=0. Hint Resolve -> a. Goal forall n, n=0 -> n<=0. auto. - -Print Hints Qed. |