Fix #848 (indentation of now tac).

For the record, in `now exists` the exists was incorrectly detected as
a "quantif exists".

Author: Matafou

ci/test-indent/indent-tac-boxed.v

@@ -153,6 +153,28 @@ Module curlybracesatend.
         simpl.
         rewrite Nat.add_1_r.
         reflexivity.
+        intros r. {
+          now exists
+                {|
+                  fld1:=r.(fld2);
+                  fld2:=r.(fld1);
+                  fld3:=false
+                |}.
+          split.
+          {auto. }
+          {auto. }
+        }
+        intros r. {
+          try exists
+                {|
+                  fld1:=r.(fld2);
+                  fld2:=r.(fld1);
+                  fld3:=false
+                |}.
+          split.
+          {auto. }
+          {auto. }
+        }
       }
     }
     idtac.

ci/test-indent/indent-tac.v

@@ -417,6 +417,28 @@ Module X.
       {auto. }
       {auto. }
     }
+    intros r. {
+      now exists
+            {|
+              fld1:=r.(fld2);
+              fld2:=r.(fld1);
+              fld3:=false
+            |}.
+      split.
+      {auto. }
+      {auto. }
+    }
+    intros r. {
+      split.
+      - now exists x.
+        split.
+        {auto. }
+        {auto. }
+      - now exists x.
+        split.
+        {auto. }
+        {auto. }
+    }
     intros r. {
       exists
         {|

coq/coq-smie.el

@@ -835,7 +835,7 @@ The point should be at the beginning of the command name."
 	     (let ((prevtok (coq-smie-backward-token)))
 	       ;; => may be wrong here but rare (have "=> ltac"?)
 	       (not (or (coq-is-cmdend-token prevtok)
-			(member prevtok '("; tactic" "[" "]" "|" "=>")))))))
+			(member prevtok '("; tactic" "[" "]" "|" "=>" "Com start")))))))
       "quantif exists")
 
      ((equal tok "∀") "forall")