diff options
| -rw-r--r-- | tactics/auto.ml | 18 | ||||
| -rw-r--r-- | tactics/class_tactics.ml4 | 2 | ||||
| -rw-r--r-- | theories/Sets/Integers.v | 1 | ||||
| -rw-r--r-- | tools/coqdoc/cpretty.mll | 4 |
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 |