Czar was an (aborted) attempt at a declarative proof mode. It never took of and has been removed now.
SSReflect is a proof language (consistent set of tactics) that is very much non-declarative since it provides a lot of shortcuts to manually do many proof management steps.
Note that Czar introduced a separate proof mode (you could not use the usual tactics within it) while SSReflect does not (you can freely mix SSReflect and non-SSReflect tactics).
Finally, let me express my (personal) opinion that Coq does not need a declarative proof mode. You can already use the current proof mode and set of tactics to produce a very declarative proof style, especially by using lots of
assert (or SSReflect’s
have) combined with lots of automation (e.g. through CoqHammer).