Merge remote-tracking branch 'origin/v8.5' into trunk

12 files changed, 212 insertions, 91 deletions

diff --git a/CHANGES b/CHANGES
index 121d906945..7f1f8b9699 100644
--- a/CHANGES
+++ b/CHANGES
@@ -23,6 +23,11 @@ Tactics
 - New compatibility flag "Universal Lemma Under Conjunction" which
   let tactics working under conjunctions apply sublemmas of the form
   "forall A, ... -> A".
+- New compatibility flag "Bracketing Last Introduction Pattern" which can be
+  set so that the last disjunctive-conjunctive introduction pattern given to
+  "intros" automatically complete the introduction of its subcomponents, as the
+  the disjunctive-conjunctive introduction patterns in non-terminal position
+  already do.
 - New flag "Shrink Abstract" that minimalizes proofs generated by the abstract
   tactical w.r.t. variables appearing in the body of the proof.
 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index fe9c582408..11f78c708c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -71,6 +71,17 @@ let make_bullet s =
   | '*' -> Star n
   | _ -> assert false
 
+(* Hack to parse "[ id" without dropping [ *)
+let test_bracket_ident =
+  Gram.Entry.of_parser "test_bracket_ident"
+    (fun strm ->
+      match get_tok (stream_nth 0 strm) with
+        | KEYWORD "[" ->
+            (match get_tok (stream_nth 1 strm) with
+              | IDENT _ -> ()
+	      | _ -> raise Stream.Failure)
+	| _ -> raise Stream.Failure)
+
 let default_command_entry =
   Gram.Entry.of_parser "command_entry"
     (fun strm -> Gram.parse_tokens_after_filter (get_command_entry ()) strm)
@@ -129,7 +140,7 @@ GEXTEND Gram
 
   selector:
     [ [ n=natural; ":" -> SelectNth n
-      | "["; id = ident; "]"; ":" -> SelectId id
+      | test_bracket_ident; "["; id = ident; "]"; ":" -> SelectId id
       | IDENT "all" ; ":" -> SelectAll
       | IDENT "par" ; ":" -> SelectAllParallel ] ]
   ;
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ef196e0a72..05e09b9686 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1466,6 +1466,14 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest =
     compile pb
   in
   let sigma = !(pb.evdref) in
+  (* If the "match" was orginally over a variable, as in "match x with
+     O => true | n => n end", we give preference to non-expansion in
+     the default clause (i.e. "match x with O => true | n => n end"
+     rather than "match x with O => true | S p => S p end";
+     computationally, this avoids reallocating constructors in cbv
+     evaluation; the drawback is that it might duplicate the instances
+     of the term to match when the corresponding variable is
+     substituted by a non-evaluated expression *)
   if not (Flags.is_program_mode ()) && (isRel orig || isVar orig) then
     (* Try to compile first using non expanded alias *)
     try
@@ -1473,6 +1481,7 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest =
       else just_pop ()
     with e when precatchable_exception e ->
     (* Try then to compile using expanded alias *)
+    (* Could be needed in case of dependent return clause *)
     pb.evdref := sigma;
     f expanded expanded_typ
   else
@@ -1480,6 +1489,8 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest =
     try f expanded expanded_typ
     with e when precatchable_exception e ->
     (* Try then to compile using non expanded alias *)
+    (* Could be needed in case of a recursive call which requires to
+       be on a variable for size reasons *)
     pb.evdref := sigma;
     if initial then f orig (Retyping.get_type_of pb.env !(pb.evdref) orig)
     else just_pop ()
diff --git a/tactics/equality.ml b/tactics/equality.ml
index d78ba8c629..ec0e1d2f4e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -540,7 +540,7 @@ let replace_core clause l2r eq =
   if check_setoid clause
   then init_setoid ();
   tclTHENFIRST
-    (assert_as false None eq)
+    (assert_as false None None eq)
     (onLastHypId (fun id ->
       tclTHEN
         (tclTRY (general_rewrite_clause l2r false (mkVar id,NoBindings) clause))
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0917a97c53..4c53d5340b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -139,6 +139,27 @@ let _ =
       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.
+   Kept as false for compatibility.
+ *)
+
+let bracketing_last_or_and_intro_pattern = ref false
+
+let use_bracketing_last_or_and_intro_pattern () =
+  !bracketing_last_or_and_intro_pattern
+  && Flags.version_strictly_greater Flags.V8_4
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "bracketing last or-and introduction pattern";
+      optkey   = ["Bracketing";"Last";"Introduction";"Pattern"];
+      optread  = (fun () -> !bracketing_last_or_and_intro_pattern);
+      optwrite = (fun b -> bracketing_last_or_and_intro_pattern := b) }
+
 (*********************************************)
 (*                 Tactics                   *)
 (*********************************************)
@@ -830,16 +851,23 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac =
   aux n []
 
 let get_next_hyp_position id gl =
-  let rec get_next_hyp_position id = function
+  let rec aux = function
   | [] -> raise (RefinerError (NoSuchHyp id))
   | (hyp,_,_) :: right ->
     if Id.equal hyp id then
       match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveLast
     else
-      get_next_hyp_position id right
+      aux right
   in
-  let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
-  get_next_hyp_position id hyps
+  aux (Proofview.Goal.hyps (Proofview.Goal.assume gl))
+
+let get_previous_hyp_position id gl =
+  let rec aux dest = function
+  | [] -> raise (RefinerError (NoSuchHyp id))
+  | (hyp,_,_) :: right ->
+    if Id.equal hyp id then dest else aux (MoveAfter hyp) right
+  in
+  aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl))
 
 let intro_replacing id =
   Proofview.Goal.enter begin fun gl ->
@@ -2107,7 +2135,7 @@ let make_tmp_naming avoid l = function
      case of IntroFresh, we should use check_thin_clash_then anyway to
      prevent the case of an IntroFresh precisely using the wild_id *)
   | IntroWildcard -> NamingBasedOn (wild_id,avoid@explicit_intro_names l)
-  | _ -> NamingAvoid(avoid@explicit_intro_names l)
+  | pat -> NamingAvoid(avoid@explicit_intro_names ((dloc,IntroAction pat)::l))
 
 let fit_bound n = function
   | None -> true
@@ -2121,6 +2149,21 @@ let exceed_bound n = function
      to ensure that dependent hypotheses are cleared in the right
      dependency order (see bug #1000); we use fresh names, not used in
      the tactic, for the hyps to clear *)
+  (* In [intro_patterns_core b avoid ids thin destopt bound n tac patl]:
+     [b]: compatibility flag, if false at toplevel, do not complete incomplete
+          trailing toplevel or_and patterns (as in "intros []", see
+          [bracketing_last_or_and_intro_pattern])
+     [avoid]: names to avoid when creating an internal name
+     [ids]: collect introduced names for possible use by the [tac] continuation
+     [thin]: collect names to erase at the end
+     [destopt]: position in the context where to introduce the hypotheses
+     [bound]: number of pending intros to do in the current or-and pattern,
+              with remembering of [b] flag if at toplevel
+     [n]: number of introduction done in the current or-and pattern
+     [tac]: continuation tactic
+     [patl]: introduction patterns to interpret
+  *)
+
 let rec intro_patterns_core b avoid ids thin destopt bound n tac = function
   | [] when fit_bound n bound ->
       tac ids thin
@@ -2138,31 +2181,33 @@ let rec intro_patterns_core b avoid ids thin destopt bound n tac = function
           (n+List.length ids) tac l)
   | IntroAction pat ->
       intro_then_gen (make_tmp_naming avoid l pat)
-	MoveLast true false
+	destopt true false
         (intro_pattern_action loc (b || not (List.is_empty l)) false pat thin
+          destopt
           (fun thin bound' -> intro_patterns_core b avoid ids thin destopt bound' 0
             (fun ids thin ->
               intro_patterns_core b avoid ids thin destopt bound (n+1) tac l)))
   | IntroNaming pat ->
-      intro_pattern_naming loc b avoid ids pat thin destopt bound n tac l
+      intro_pattern_naming loc b avoid ids pat thin destopt bound (n+1) tac l
 
+  (* Pi-introduction rule, used backwards *)
 and intro_pattern_naming loc b avoid ids pat thin destopt bound n tac l =
   match pat with
   | IntroIdentifier id ->
       check_thin_clash_then id thin avoid (fun thin ->
         intro_then_gen (NamingMustBe (loc,id)) destopt true false
-          (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound (n+1) tac l))
+          (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound n tac l))
   | IntroAnonymous ->
       intro_then_gen (NamingAvoid (avoid@explicit_intro_names l))
 	destopt true false
-        (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound (n+1) tac l)
+        (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound n tac l)
   | IntroFresh id ->
       (* todo: avoid thinned names to interfere with generation of fresh name *)
       intro_then_gen (NamingBasedOn (id, avoid@explicit_intro_names l))
 	destopt true false
-        (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound (n+1) tac l)
+        (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound n tac l)
 
-and intro_pattern_action loc b style pat thin tac id = match pat with
+and intro_pattern_action loc b style pat thin destopt tac id = match pat with
   | IntroWildcard ->
       tac ((loc,id)::thin) None []
   | IntroOrAndPattern ll ->
@@ -2175,7 +2220,8 @@ and intro_pattern_action loc b style pat thin tac id = match pat with
 	(rewrite_hyp style l2r id)
         (tac thin None [])
   | IntroApplyOn (f,(loc,pat)) ->
-      let naming,tac_ipat = prepare_intros_loc loc (IntroIdentifier id) pat in
+      let naming,tac_ipat =
+        prepare_intros_loc loc (IntroIdentifier id) destopt pat in
       Proofview.Goal.enter begin fun gl ->
         let sigma = Proofview.Goal.sigma gl in
         let env = Proofview.Goal.env gl in
@@ -2184,36 +2230,29 @@ and intro_pattern_action loc b style pat thin tac id = match pat with
           (Tacticals.New.tclTHENFIRST
              (* Skip the side conditions of the apply *)
              (apply_in_once false true true true naming id
-                (None,(sigma,(c,NoBindings))) tac_ipat) (tac thin None []))
+                (None,(sigma,(c,NoBindings))) tac_ipat) (tac ((dloc,id)::thin) None []))
           sigma
       end
 
-and prepare_intros_loc loc dft = function
+and prepare_intros_loc loc dft destopt = function
   | IntroNaming ipat ->
       prepare_naming loc ipat,
-      (fun _ -> Proofview.tclUNIT ())
+      (fun id -> Proofview.V82.tactic (move_hyp id destopt))
   | IntroAction ipat ->
       prepare_naming loc dft,
       (let tac thin bound =
-        intro_patterns_core true [] [] thin MoveLast bound 0
+        intro_patterns_core true [] [] thin destopt bound 0
           (fun _ l -> clear_wildcards l) in
-      fun id -> intro_pattern_action loc true true ipat [] tac id)
+      fun id -> intro_pattern_action loc true true ipat [] destopt tac id)
   | IntroForthcoming _ -> user_err_loc
       (loc,"",str "Introduction pattern for one hypothesis expected.")
 
 let intro_patterns_bound_to n destopt =
   intro_patterns_core true [] [] [] destopt
-    (Some (true,n)) 0 (fun _ -> clear_wildcards)
-
-(* 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.
-   Kept as false for compatibility.
- *)
-let bracketing_last_or_and_intro_pattern = false 
+    (Some (true,n)) 0 (fun _ l -> clear_wildcards l)
 
 let intro_patterns_to destopt =
-  intro_patterns_core bracketing_last_or_and_intro_pattern
+  intro_patterns_core (use_bracketing_last_or_and_intro_pattern ())
     [] [] [] destopt None 0 (fun _ l -> clear_wildcards l)
 
 let intro_pattern_to destopt pat =
@@ -2230,23 +2269,24 @@ let intros_patterns = function
 (*   Forward reasoning    *)
 (**************************)
 
-let prepare_intros dft = function
+let prepare_intros dft destopt = function
   | None -> prepare_naming dloc dft, (fun _id -> Proofview.tclUNIT ())
-  | Some (loc,ipat) -> prepare_intros_loc loc dft ipat
+  | Some (loc,ipat) -> prepare_intros_loc loc dft destopt ipat
 
 let ipat_of_name = function
   | Anonymous -> None
   | Name id -> Some (dloc, IntroNaming (IntroIdentifier id))
 
- let head_ident c =
+let head_ident c =
    let c = fst (decompose_app ((strip_lam_assum c))) in
    if isVar c then Some (destVar c) else None
 
-let assert_as first ipat c =
-  let naming,tac = prepare_intros IntroAnonymous ipat in
-  let repl = do_replace (head_ident c) naming in
-  if first then assert_before_then_gen repl naming c tac
-  else assert_after_then_gen repl naming c tac
+let assert_as first hd ipat t =
+  let naming,tac = prepare_intros IntroAnonymous MoveLast ipat in
+  let repl = do_replace hd naming in
+  let tac = if repl then (fun id -> Proofview.tclUNIT ()) else tac in
+  if first then assert_before_then_gen repl naming t tac
+  else assert_after_then_gen repl naming t tac
 
 (* apply in as *)
 
@@ -2255,13 +2295,16 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars
   let tac (naming,lemma) tac id =
     apply_in_delayed_once sidecond_first with_delta with_destruct with_evars
       naming id lemma tac in
-  let naming,ipat_tac = prepare_intros (IntroIdentifier id) ipat in
+  Proofview.Goal.enter begin fun gl ->
+  let destopt = get_previous_hyp_position id gl in
+  let naming,ipat_tac = prepare_intros (IntroIdentifier id) destopt ipat in
   let lemmas_target, last_lemma_target =
     let last,first = List.sep_last lemmas in
     List.map (fun lem -> (NamingMustBe (dloc,id),lem)) first, (naming,last)
   in
   (* We chain apply_in_once, ending with an intro pattern *)
   List.fold_right tac lemmas_target (tac last_lemma_target ipat_tac) id
+  end
 
 (*
   if sidecond_first then
@@ -2406,16 +2449,17 @@ let forward b usetac ipat c =
   match usetac with
   | None ->
       Proofview.Goal.enter begin fun gl ->
-      let t = Tacmach.New.pf_unsafe_type_of gl  c in
-      Tacticals.New.tclTHENFIRST (assert_as true ipat t)
+      let t = Tacmach.New.pf_unsafe_type_of gl c in
+      let hd = head_ident c in
+      Tacticals.New.tclTHENFIRST (assert_as true hd ipat t)
 	(Proofview.V82.tactic (exact_no_check c))
       end
   | Some tac ->
       if b then
-        Tacticals.New.tclTHENFIRST (assert_as b ipat c) tac
+        Tacticals.New.tclTHENFIRST (assert_as b None ipat c) tac
       else
         Tacticals.New.tclTHENS3PARTS
-          (assert_as b ipat c) [||] tac [|Tacticals.New.tclIDTAC|]
+          (assert_as b None ipat c) [||] tac [|Tacticals.New.tclIDTAC|]
 
 let pose_proof na c = forward true None (ipat_of_name na) c
 let assert_by na t tac = forward true (Some tac) (ipat_of_name na) t
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 0069d100b7..ade89fc989 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -348,6 +348,7 @@ val assert_before : Name.t -> types -> unit Proofview.tactic
 val assert_after  : Name.t -> types -> unit Proofview.tactic
 
 val assert_as     : (* true = before *) bool ->
+  (* optionally tell if a specialization of some hyp: *) identifier option ->
   intro_pattern option -> constr -> unit Proofview.tactic
 
 (** Implements the tactics assert, enough and pose proof; note that "by"
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 074004fa12..55b666b723 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -548,3 +548,14 @@ apply (foo ?y).
 Grab Existential Variables.
 exact 0.
 Qed.
+
+(* Test position of new hypotheses when using "apply ... in ... as ..." *)
+Goal (True -> 0=0 /\ True) -> True -> False -> True/\0=0.
+intros H H0 H1.
+apply H in H0 as (a,b).
+(* clear H1:False *) match goal with H:_ |- _ => clear H end.
+split.
+- (* use b:True *) match goal with H:_ |- _ => exact H end.
+- (* clear b:True *) match goal with H:_ |- _ => clear H end.
+  (* use a:0=0 *) match goal with H:_ |- _ => exact H end.
+Qed.
diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index 9443d01e3b..ae1694c58c 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -33,3 +33,31 @@ Goal True -> True -> True.
 intros _ ?.
 exact H.
 Qed.
+
+(* A short test about introduction pattern pat/c *)
+Goal (True -> 0=0) -> True /\ False -> 0=0.
+intros H (H1/H,_).
+exact H1.
+Qed.
+
+(* A test about bugs in 8.5beta2 *)
+Goal (True -> 0=0) -> True /\ False -> False -> 0=0.
+intros H H0 H1.
+destruct H0 as (a/H,_).
+(* Check that H0 is removed (was bugged in 8.5beta2) *)
+Fail clear H0.
+(* Check position of newly created hypotheses when using pat/c (was
+   left at top in 8.5beta2) *)
+match goal with H:_ |- _ => clear H end. (* clear H1:False *)
+match goal with H:_ |- _ => exact H end. (* check that next hyp shows 0=0 *)
+Qed.
+
+Goal (True -> 0=0) -> True -> 0=0.
+intros H H1/H.
+exact H1.
+Qed.
+
+Goal forall n, n = S n -> 0=0.
+intros n H/n_Sn.
+destruct H.
+Qed.
diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v
index c5f032beb0..3faa1ca43a 100644
--- a/test-suite/success/specialize.v
+++ b/test-suite/success/specialize.v
@@ -45,4 +45,22 @@ specialize eq_trans with _ a b c. intros _.
 (* Anomaly: Evar ?88 was not declared. Please report. *)
 *)
 
-Abort.
\ No newline at end of file
+Abort.
+
+(* Test use of pose proof and assert as a specialize *)
+
+Goal True -> (True -> 0=0) -> False -> 0=0.
+intros H0 H H1.
+pose proof (H I) as H.
+(* Check that the hypothesis is in 2nd position by removing the top one *)
+match goal with H:_ |- _ => clear H end.
+match goal with H:_ |- _ => exact H end.
+Qed.
+
+Goal True -> (True -> 0=0) -> False -> 0=0.
+intros H0 H H1.
+assert (H:=H I).
+(* Check that the hypothesis is in 2nd position by removing the top one *)
+match goal with H:_ |- _ => clear H end.
+match goal with H:_ |- _ => exact H end.
+Qed.
diff --git a/theories/Logic/WeakFan.v b/theories/Logic/WeakFan.v
index 49cc12b85a..2f84ebe5f3 100644
--- a/theories/Logic/WeakFan.v
+++ b/theories/Logic/WeakFan.v
@@ -89,17 +89,14 @@ Qed.
 Theorem WeakFanTheorem : forall P, barred P -> inductively_barred P [].
 Proof.
 intros P Hbar.
-destruct (Hbar (X P)) as (l,(Hd,HP)).
+destruct Hbar with (X P) as (l,(Hd/Y_approx,HP)).
 assert (inductively_barred P l) by (apply (now P l), HP).
 clear Hbar HP.
-induction l.
+induction l as [|a l].
 - assumption.
 - destruct Hd as (Hd,HX).
   apply (IHl Hd). clear IHl.
   destruct a; unfold X in HX; simpl in HX.
-  + apply propagate.
-    * apply H.
-    * destruct HX as (l',(Hl,(HY,Ht))); firstorder.
-      apply Y_approx in Hd. rewrite <- (Y_unique P l' l Hl); trivial.
-  + destruct HX. exists l. split; auto using Y_approx.
+  + apply propagate; assumption.
+  + exfalso; destruct (HX H).
 Qed.
diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v
index b9bf6c7f7e..2955184f6b 100644
--- a/theories/Vectors/Fin.v
+++ b/theories/Vectors/Fin.v
@@ -152,18 +152,18 @@ Fixpoint L {m} n (p : t m) : t (m + n) :=
 Lemma L_sanity {m} n (p : t m) : proj1_sig (to_nat (L n p)) = proj1_sig (to_nat p).
 Proof.
 induction p.
-  reflexivity.
-  simpl; destruct (to_nat (L n p)); simpl in *; rewrite IHp. now destruct (to_nat p).
+- reflexivity.
+- simpl; destruct (to_nat (L n p)); simpl in *; rewrite IHp. now destruct (to_nat p).
 Qed.
-
+ 
 (** The p{^ th} element of [fin m] viewed as the p{^ th} element of
 [fin (n + m)]
 Really really ineficient !!! *)
 Definition L_R {m} n (p : t m) : t (n + m).
 Proof.
 induction n.
-  exact p.
-  exact ((fix LS k (p: t k) :=
+- exact p.
+- exact ((fix LS k (p: t k) :=
     match p with
       |@F1 k' => @F1 (S k')
       |FS p' => FS (LS _ p')
@@ -178,8 +178,8 @@ Fixpoint R {m} n (p : t m) : t (n + m) :=
 Lemma R_sanity {m} n (p : t m) : proj1_sig (to_nat (R n p)) = n + proj1_sig (to_nat p).
 Proof.
 induction n.
-  reflexivity.
-  simpl; destruct (to_nat (R n p)); simpl in *; rewrite IHn. now destruct (to_nat p).
+- reflexivity.
+- simpl; destruct (to_nat (R n p)); simpl in *; rewrite IHn. now destruct (to_nat p).
 Qed.
 
 Fixpoint depair {m n} (o : t m) (p : t n) : t (m * n) :=
@@ -192,9 +192,9 @@ Lemma depair_sanity {m n} (o : t m) (p : t n) :
   proj1_sig (to_nat (depair o p)) = n * (proj1_sig (to_nat o)) + (proj1_sig (to_nat p)).
 Proof.
 induction o ; simpl.
-  rewrite L_sanity. now rewrite Mult.mult_0_r.
+- rewrite L_sanity. now rewrite Mult.mult_0_r.
 
-  rewrite R_sanity. rewrite IHo.
+- rewrite R_sanity. rewrite IHo.
   rewrite Plus.plus_assoc. destruct (to_nat o); simpl; rewrite Mult.mult_succ_r.
     now rewrite (Plus.plus_comm n).
 Qed.
@@ -210,10 +210,10 @@ end.
 Lemma eqb_nat_eq : forall m n (p : t m) (q : t n), eqb p q = true -> m = n.
 Proof.
 intros m n p; revert n; induction p; destruct q; simpl; intros; f_equal.
-+ now apply EqNat.beq_nat_true.
-+ easy.
-+ easy.
-+ eapply IHp. eassumption.
+- now apply EqNat.beq_nat_true.
+- easy.
+- easy.
+- eapply IHp. eassumption.
 Qed.
 
 Lemma eqb_eq : forall n (p q : t n), eqb p q = true <-> p = q.
@@ -231,9 +231,9 @@ Qed.
 
 Lemma eq_dec {n} (x y : t n): {x = y} + {x <> y}.
 Proof.
- case_eq (eqb x y); intros.
-  + left; now apply eqb_eq.
-  + right. intros Heq. apply <- eqb_eq in Heq. congruence.
+case_eq (eqb x y); intros.
+- left; now apply eqb_eq.
+- right. intros Heq. apply <- eqb_eq in Heq. congruence.
 Defined.
 
 Definition cast: forall {m} (v: t m) {n}, m = n -> t n.
diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v
index 46b537737e..c5278b918f 100644
--- a/theories/Vectors/VectorSpec.v
+++ b/theories/Vectors/VectorSpec.v
@@ -24,12 +24,7 @@ Definition cons_inj {A} {a1 a2} {n} {v1 v2 : t A n}
 
 Lemma eta {A} {n} (v : t A (S n)) : v = hd v :: tl v.
 Proof.
-  change
-    (match S n with
-    | 0 => fun v : t A 0 => v = v
-    | S n => fun v => v = hd v :: tl v
-    end v).
-  destruct v; reflexivity.
+intros; apply caseS with (v:=v); intros; reflexivity.
 Defined.
 
 (** Lemmas are done for functions that use [Fin.t] but thanks to [Peano_dec.le_unique], all
@@ -39,12 +34,12 @@ Lemma eq_nth_iff A n (v1 v2: t A n):
   (forall p1 p2, p1 = p2 -> v1 [@ p1 ] = v2 [@ p2 ]) <-> v1 = v2.
 Proof.
 split.
-  revert n v1 v2; refine (@rect2 _ _ _ _ _); simpl; intros.
-    reflexivity.
-    f_equal. apply (H0 Fin.F1 Fin.F1 eq_refl).
+- revert n v1 v2; refine (@rect2 _ _ _ _ _); simpl; intros.
+  + reflexivity.
+  + f_equal. apply (H0 Fin.F1 Fin.F1 eq_refl).
     apply H. intros p1 p2 H1;
     apply (H0 (Fin.FS p1) (Fin.FS p2) (f_equal (@Fin.FS n) H1)).
-  intros; now f_equal.
+- intros; now f_equal.
 Qed.
 
 Lemma nth_order_last A: forall n (v: t A (S n)) (H: n < S n),
@@ -57,8 +52,8 @@ Lemma shiftin_nth A a n (v: t A n) k1 k2 (eq: k1 = k2):
   nth (shiftin a v) (Fin.L_R 1 k1) = nth v k2.
 Proof.
 subst k2; induction k1.
-  generalize dependent n. apply caseS ; intros. now simpl.
-  generalize dependent n. refine (@caseS _ _ _) ; intros. now simpl.
+- generalize dependent n. apply caseS ; intros. now simpl.
+- generalize dependent n. refine (@caseS _ _ _) ; intros. now simpl.
 Qed.
 
 Lemma shiftin_last A a n (v: t A n): last (shiftin a v) = a.
@@ -70,8 +65,8 @@ Lemma shiftrepeat_nth A: forall n k (v: t A (S n)),
   nth (shiftrepeat v) (Fin.L_R 1 k) = nth v k.
 Proof.
 refine (@Fin.rectS _ _ _); lazy beta; [ intros n v | intros n p H v ].
-  revert n v; refine (@caseS _ _ _); simpl; intros. now destruct t.
-  revert p H.
+- revert n v; refine (@caseS _ _ _); simpl; intros. now destruct t.
+- revert p H.
   refine (match v as v' in t _ m return match m as m' return t A m' -> Prop with
     |S (S n) => fun v => forall p : Fin.t (S n),
       (forall v0 : t A (S n), (shiftrepeat v0) [@ Fin.L_R 1 p ] = v0 [@p]) ->
@@ -94,8 +89,8 @@ Lemma nth_map {A B} (f: A -> B) {n} v (p1 p2: Fin.t n) (eq: p1 = p2):
   (map f v) [@ p1] = f (v [@ p2]).
 Proof.
 subst p2; induction p1.
-  revert n v; refine (@caseS _ _ _); now simpl.
-  revert n v p1 IHp1; refine (@caseS _  _ _); now simpl.
+- revert n v; refine (@caseS _ _ _); now simpl.
+- revert n v p1 IHp1; refine (@caseS _  _ _); now simpl.
 Qed.
 
 Lemma nth_map2 {A B C} (f: A -> B -> C) {n} v w (p1 p2 p3: Fin.t n):
@@ -103,8 +98,8 @@ Lemma nth_map2 {A B C} (f: A -> B -> C) {n} v w (p1 p2 p3: Fin.t n):
 Proof.
 intros; subst p2; subst p3; revert n v w p1.
 refine (@rect2 _ _ _ _ _); simpl.
-  exact (Fin.case0 _).
-  intros n v1 v2 H a b p; revert n p v1 v2 H; refine (@Fin.caseS _ _ _);
+- exact (Fin.case0 _).
+- intros n v1 v2 H a b p; revert n p v1 v2 H; refine (@Fin.caseS _ _ _);
     now simpl.
 Qed.
 
@@ -113,17 +108,17 @@ Lemma fold_left_right_assoc_eq {A B} {f: A -> B -> A}
   {n} (v: t B n): forall a, fold_left f a v = fold_right (fun x y => f y x) v a.
 Proof.
 assert (forall n h (v: t B n) a, fold_left f (f a h) v = f (fold_left f a v) h).
-  induction v0.
-    now simpl.
-    intros; simpl. rewrite<- IHv0, assoc. now f_equal.
-  induction v.
-    reflexivity.
-    simpl. intros; now rewrite<- (IHv).
+- induction v0.
+  + now simpl.
+  + intros; simpl. rewrite<- IHv0, assoc. now f_equal.
+- induction v.
+  + reflexivity.
+  + simpl. intros; now rewrite<- (IHv).
 Qed.
 
 Lemma to_list_of_list_opp {A} (l: list A): to_list (of_list l) = l.
 Proof.
 induction l.
-  reflexivity.
-  unfold to_list; simpl. now f_equal.
+- reflexivity.
+- unfold to_list; simpl. now f_equal.
 Qed.