aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-12-01 16:36:52 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-12-01 16:36:52 +0000
commitda882cfdac822da8d53e8c11b4a890e1643901ad (patch)
treee6cccb3c121feeefa0e26ef4b287fa334dbe5256
parent0780de3f579681aa80e5e353d3aaeeaa418f2369 (diff)
Fix make_exact_entry to allow applying [forall x, P x] hints directly,
avoiding the introduction of eta-redexes. Prioritize hints over intros in typeclass resolution to profit from that. Add a minor fix in coqdoc by F. Garillot. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12550 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--tactics/auto.ml18
-rw-r--r--tactics/class_tactics.ml42
-rw-r--r--theories/Sets/Integers.v1
-rw-r--r--tools/coqdoc/cpretty.mll4
4 files changed, 11 insertions, 14 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 92750094c..b6dc4e598 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -270,22 +270,20 @@ let dummy_goal =
let make_exact_entry pri (c,cty) =
let cty = strip_outer_cast cty in
- match kind_of_term cty with
- | Prod (_,_,_) ->
- failwith "make_exact_entry"
- | _ ->
- let ce = mk_clenv_from dummy_goal (c,cty) in
- let c' = clenv_type ce in
- let pat = Pattern.pattern_of_constr c' in
- (Some (head_of_constr_reference (fst (head_constr cty))),
- { pri=(match pri with Some pri -> pri | None -> 0); pat=Some pat; code=Give_exact c })
+ let pat = Pattern.pattern_of_constr cty in
+ let head =
+ try head_of_constr_reference (fst (head_constr cty))
+ with _ -> failwith "make_exact_entry"
+ in
+ (Some head,
+ { pri=(match pri with Some pri -> pri | None -> 0); pat=Some pat; code=Give_exact c })
let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) =
let cty = if hnf then hnf_constr env sigma cty else cty in
match kind_of_term cty with
| Prod _ ->
let ce = mk_clenv_from dummy_goal (c,cty) in
- let c' = clenv_type ce in
+ let c' = clenv_type (* ~reduce:false *) ce in
let pat = Pattern.pattern_of_constr c' in
let hd = (try head_pattern_bound pat
with BoundPattern -> failwith "make_apply_entry") in
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 4d367ac61..bd632b59a 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -452,7 +452,7 @@ let run_on_evars ?(only_classes=true) ?(st=full_transparent_state) p evm tac =
| Some (evm', fk) -> Some (Evd.evars_reset_evd evm' evm, fk)
let eauto_tac hints =
- fix (or_tac intro_tac (then_tac normevars_tac (hints_tac hints)))
+ fix (or_tac (then_tac normevars_tac (hints_tac hints)) intro_tac)
let eauto ?(only_classes=true) ?st hints g =
let gl = { it = make_autogoal ~only_classes ?st None g; sigma = project g } in
diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v
index 443713211..01d3bda37 100644
--- a/theories/Sets/Integers.v
+++ b/theories/Sets/Integers.v
@@ -79,7 +79,6 @@ Section Integers_sect.
auto with sets arith.
apply Inhabited_intro with (x := 0).
apply Integers_defn.
- exact le_Order.
Defined.
Lemma le_total_order : Totally_ordered nat nat_po Integers.
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 4742a2e5d..4f1406cc8 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -184,10 +184,10 @@
let check_start_list str =
let n_dashes = count_dashes str in
let (n_spaces,_) = count_spaces str in
- if n_dashes >= 4 then
+ if n_dashes >= 4 && not !Cdglobals.plain_comments then
Rule
else
- if n_dashes = 1 then
+ if n_dashes = 1 && not !Cdglobals.plain_comments then
List n_spaces
else
Neither